Loading...
Conflict-preserving abstraction of discrete event systems using annotated automata
Abstract
This paper proposes to enhance compositional verification of the nonblocking property of discrete event systems by introducing annotated automata. Annotations store nondeterministic branching information, which would otherwise be stored in extra states and transitions. This succinct representation makes it easier to simplify automata and enables new efficientmeans of abstraction, reducing the size of automata to be composed and thus the size of the synchronous product state space encountered in verification. The abstractions proposed are of polynomial complexity, and they have been successfully applied to model check the nonblocking property of the same set of large-scale industrial examples as used in related work.
Type
Journal Article
Type of thesis
Series
Citation
Ware, S. & Malik, R. (2012). Conflict-preserving abstraction of discrete event systems using annotated automata. Discrete Event Dynamic Systems, 22(4), 451-477.
Date
2012
Publisher
Springer
Degree
Supervisors
Rights
This is an author’s accepted version of an article published in the journal: Discrete Event Dynamic Systems. © 2012 Springer.