Conflict-preserving abstraction of discrete event systems using annotated automata

DOI10.1007/s10626-012-0133-3zbMath1267.93111OpenAlexW2085821685MaRDI QIDQ351736

Simon Ware, Robi Malik

Publication date: 9 July 2013

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/10289/6387

zbMATH Keywords

model checkingdiscrete event systemsnonblockingfinite state machines

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Applications of graph theory to circuits and networks (94C15)

Related Items

A survey on compositional algorithms for verification and synthesis in supervisory control ⋮ On the computation of counterexamples in compositional nonblocking verification ⋮ Progressive events in supervisory control and compositional verification ⋮ Hierarchical modelling of manufacturing systems using discrete event systems and the conflict preorder

Uses Software

• UMDES
• Supremica

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fair testing
• An implementation of an efficient algorithm for bisimulation equivalence
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Specification-oriented semantics for communicating processes
• Minimizing the number of transitions with respect to observation equivalence
• Testing equivalences for processes
• Compositional Verification in Supervisory Control
• Supervisory Control Architecture for Discrete-Event Systems
• Verification of Nonconflict of Supervisors Using Abstractions
• CONFLICTS AND FAIR TESTING