Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

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

Résumé

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.
Fichier principal
Vignette du fichier
478668_1_En_9_Chapter.pdf (1.01 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02313740 , version 1 (11-10-2019)

Licence

Paternité

Identifiants

Citer

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⟩
48 Consultations
18 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More