Abstract
Hybrid Petri nets have been extended with so-called general transitions, which add one random variable and one dimension to the underlying state space for each firing of a general transition. We propose an algorithm for model checking the time-bounded until operator in hybrid Petri nets with two general transition firings, based on boolean-set operations on Nef polyhedra. A case study on (dis)-charging an electrical vehicle shows the feasibility of the approach. Results are validated against a simulation tool and computation times are compared.
Cite
CITATION STYLE
Godde, A., & Remke, A. (2017). Model checking the STL time-bounded until on hybrid petri nets using nef polyhedra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10497 LNCS, pp. 101–116). Springer Verlag. https://doi.org/10.1007/978-3-319-66583-2_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
