%0 Conference Proceedings
%T Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes
%+ Westfälische Wilhelms-Universität Münster = University of Münster (WWU)
%A Hüls, Jannik
%A Remke, Anne
%Z Part 1: Full Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-11535
%P 148-166
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_9
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313740/document
%2 https://inria.hal.science/hal-02313740/file/478668_1_En_9_Chapter.pdf
%L hal-02313740
%U https://inria.hal.science/hal-02313740
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535