Conflict-preserving abstraction of discrete event systems using annotated automata

DOI10.1007/S10626-012-0133-3MaRDI QIDQ351736zbMATH OpenOpenAlexFDO

Authors 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

discrete event systemsfinite state machinesmodel checkingnonblocking

Mathematics Subject Classification ID

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

Recommendations

• Compositional verification in supervisory control
• A framework for compositional nonblocking verification of extended finite-state machines
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Compositional coordinator synthesis of extended finite automata

Cites work

• An implementation of an efficient algorithm for bisimulation equivalence
• Compositional verification in supervisory control
• CONFLICTS AND FAIR TESTING
• Fair testing
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1383199 (Why is no real title available?)
• scientific article; zbMATH DE number 813252 (Why is no real title available?)
• Minimizing the number of transitions with respect to observation equivalence
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Specification-oriented semantics for communicating processes
• Supervisory Control Architecture for Discrete-Event Systems
• Testing equivalences for processes
• Verification of Nonconflict of Supervisors Using Abstractions

Cited in

(9)

• On the computation of counterexamples in compositional nonblocking verification
• Hierarchical modelling of manufacturing systems using discrete event systems and the conflict preorder
• A framework for compositional nonblocking verification of extended finite-state machines
• Compositional verification in supervisory control
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• Progressive events in supervisory control and compositional verification
• A survey on compositional algorithms for verification and synthesis in supervisory control
• Compositional non-blockingness verification of finite automata with prioritised events
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence

Describes a project that uses

Uses Software

• UMDES
• Supremica

This page was built for publication: Conflict-preserving abstraction of discrete event systems using annotated automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q351736)