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

10Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Hüls, J., & Remke, A. (2019). Model Checking HPnGs in Multiple Dimensions: Representing State Sets as Convex Polytopes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11535 LNCS, pp. 148–166). Springer Verlag. https://doi.org/10.1007/978-3-030-21759-4_9

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free