On the computation of counterexamples in compositional nonblocking verification

DOI10.1007/S10626-019-00305-WMaRDI QIDQ2197583zbMATH OpenOpenAlexWikidataFDO

Authors Robi Malik, Simon Ware

Publication date 1 September 2020

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

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

zbMATH Keywords

compositional verificationdiscrete event systemsmodel checkingnonblocking

Mathematics Subject Classification ID

Computational methods for problems pertaining to systems and control theory (93-08) Discrete event control/observation systems (93C65)

Recommendations

• Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• A framework for compositional nonblocking verification of extended finite-state machines
• Compositional verification of termination-preserving refinement of concurrent programs
• Compositional model checking with incremental counter-example construction
• A compositional approach to CTL^* verification
• Compositional verification of concurrent systems by combining bisimulations
• Automata, Languages and Programming
• On verifying that a concurrent program satisfies a nondeterministic specification

Cites work

• Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
• Compositional verification in supervisory control
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• Compositionality in state space verification methods
• Conflict-preserving abstraction of discrete event systems using annotated automata
• CONFLICTS AND FAIR TESTING
• scientific article; zbMATH DE number 1633145 (Why is no real title available?)
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 4033041 (Why is no real title available?)
• 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 177514 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• Introduction to Discrete Event Systems
• Logic in Computer Science
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Testing equivalences for processes
• Verification of Nonconflict of Supervisors Using Abstractions

Cited in

(6)

• scientific article; zbMATH DE number 65749 (Why is no real title available?)
• Compositional safety refutation techniques
• Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
• A survey on compositional algorithms for verification and synthesis in supervisory control
• Compositional non-blockingness verification of finite automata with prioritised events
• Offline supervisory control synthesis: taxonomy and recent developments

Describes a project that uses

Uses Software

• Supremica
• UMDES

This page was built for publication: On the computation of counterexamples in compositional nonblocking verification

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