Compositional verification in supervisory control

DOI10.1137/070695526zbMATH Open1282.93176OpenAlexW2016140364MaRDI QIDQ3566992FDOQ3566992

Authors Hugo Flordal, Robi Malik

Publication date 10 June 2010

Published in SIAM Journal on Control and Optimization (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/070695526

zbMATH Keywords

model checkingdiscrete-event systemsnonblockingsupervisory control

Mathematics Subject Classification ID

Controllability (93B05) Specification and verification (program logics, model checking, etc.) (68Q60) Hierarchical systems (93A13) Discrete event control/observation systems (93C65)

Recommendations

• A survey on compositional algorithms for verification and synthesis in supervisory control
• A framework for compositional nonblocking verification of extended finite-state machines
• Conflict-preserving abstraction of discrete event systems using annotated automata
• Progressive events in supervisory control and compositional verification
• scientific article; zbMATH DE number 1836359

Cited in

(21)

• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Hierarchical modelling of manufacturing systems using discrete event systems and the conflict preorder
• Progressive events in supervisory control and compositional verification
• On conditional decomposability
• Supervisory control of discrete event systems with distinguishers
• Compositional non-blockingness verification of finite automata with prioritised events
• Compositional coordinator synthesis of extended finite automata
• State complexity of projected languages
• Time-optimal control of large-scale systems of systems using compositional optimization
• On the computation of counterexamples in compositional nonblocking verification
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• On a structural property in the state complexity of projected regular languages
• Conflict-preserving abstraction of discrete event systems using annotated automata
• Incremental verification for on-the-fly controller synthesis
• Verification of Supervisory Control Software Using State Proximity and Merging
• Conceptual design of discrete-event systems using templates
• On-the-fly informed search of non-blocking directed controllers
• A survey on compositional algorithms for verification and synthesis in supervisory control
• Compositional synthesis of supervisors in the form of state machines and state maps
• A framework for compositional nonblocking verification of extended finite-state machines
• Modular supervisory control with equivalence-based abstraction and covering-based conflict resolution

This page was built for publication: Compositional verification in supervisory control

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