Complexity issues in automata theoretic verification

MaRDI QIDQ4503922zbMATH OpenFDO

Authors Sandeep Kumar Shukla

Publication date 6 December 2000

zbMATH Keywords

COSPANprogram verificationw-automaton

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The paper deals with the automata theoretic approach to linear time based verification methodology, where computation is viewed as a set of linear sequences of events. The \(\omega\)-automaton is used as a basic theoretical tool. The COSPAN software verification tool is briefly described. In the first part of the paper a brief tutorial of using the COSPAN is given. The COSPAN is oriented specially to the algorithmic analysis of finite-state linear time models. It includes refinement and abstraction techniques, as well as decomposition and localization tools. Conversion of the \(\omega\)-automata description of a system semantics to S/R language used by COSPAN is shown. Several methodological examples illustrate applications of COSPAN. In the second part the mathematical background of the above methodology is presented. So-called L-process and L-automaton are defined for formal description of system semantics. Several theoretical results concerning mainly determinism and modularity issues are proven. For the entire collection see [Zbl 0935.00051].

Recommendations

• The automata-theoretic approach to verification of reactive systems
• scientific article; zbMATH DE number 734956
• Software model checking
• Automata- and logic-based systems design
• Automata theory and model checking

Cited in

(8)

• The automata-theoretic approach to verification of reactive systems
• Computational complexity of decision problems on self-verifying finite automata
• Logics and automata for verification: Expressiveness and decidability issues
• Complexity of some problems from the theory of automata
• scientific article; zbMATH DE number 4026835 (Why is no real title available?)
• scientific article; zbMATH DE number 4047135 (Why is no real title available?)
• scientific article; zbMATH DE number 7440191 (Why is no real title available?)
• scientific article; zbMATH DE number 7577577 (Why is no real title available?)

This page was built for publication: Complexity issues in automata theoretic verification

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