Skip to Main content Skip to Navigation
Conference papers

Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes

Abstract : Hybrid Petri Nets with general transitions (HPnG) include general transitions that fire after a randomly distributed amount of time. Stochastic Time Logic (STL) expresses properties that can be model checked using a symbolic representation for sets of states as convex polytopes. Model checking then performs geometric operations on convex polytopes. The implementation of previous approaches was restricted to two stochastic firings. This paper instead proposes model checking algorithms for HPnGs with an arbitrary but finite number of stochastic firings and features an implementation based on the library HyPro.
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-02313740
Contributor : Hal Ifip <>
Submitted on : Friday, October 11, 2019 - 2:55:24 PM
Last modification on : Friday, October 11, 2019 - 3:43:39 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Jannik Hüls, Anne Remke. Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.148-166, ⟨10.1007/978-3-030-21759-4_9⟩. ⟨hal-02313740⟩

Share

Metrics

Record views

42