Efficiency of automata in semi-commutation verification techniques

DOI10.1051/ita:2007029zbMath1144.68039MaRDI QIDQ3515458

Yann Mainier, Gérard Cécé, Pierre-Cyrille Héam

Publication date: 29 July 2008

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/245200

zbMATH Keywords

model checking; transitive closure; image of a regular language

Mathematics Subject Classification ID

68Q45: Formal languages and automata

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

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

State Complexity of Permutation and the Language Inclusion Problem up to Parikh Equivalence on Alphabetical Pattern Constraints and Partially Ordered NFAs, Regular languages and partial commutations, A note on partially ordered tree automata, The commutative closure of shuffle languages over group languages is regular

Uses Software

• OCaml

Cites Work

• Permutation rewriting and algorithmic verification
• Classification of finite monoids: the language approach
• Classifying regular events in symbolic logic
• Variétés de langages et opérations
• A partial approach to model checking
• Polynomial closure and unambiguous product
• Modeling literal morphisms by shuffle
• Some complexity results for polynomial rational expressions.
• Shuffle on positive varieties of languages
• Finite semigroup varieties of the form V*D
• Characterizations of locally testable events
• Regular Model Checking using Widening Techniques
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item