COMPOSITIONAL VERIFICATION OF THE GENERALIZED NONBLOCKING PROPERTY USING ABSTRACTION AND CANONICAL AUTOMATA

DOI10.1142/S0129054113500287zbMath1291.68270MaRDI QIDQ5168410

Simon Ware, Robi Malik

Publication date: 4 July 2014

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s0129054113500287

zbMATH Keywords

model checking; finite-state machines; nonblocking; process-algebra

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

A survey on compositional algorithms for verification and synthesis in supervisory control, On the computation of counterexamples in compositional nonblocking verification

Cites Work

• An implementation of an efficient algorithm for bisimulation equivalence
• Nonconflict check by using sequential automaton abstractions based on weak observation equivalence
• Testing equivalences for processes
• Compositional Verification in Supervisory Control
• Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
• CONFLICTS AND FAIR TESTING
• Derivatives of Regular Expressions