Permutation rewriting and algorithmic verification

DOI10.1016/j.ic.2005.11.007zbMath1107.68052OpenAlexW2063288032MaRDI QIDQ865624

Tayssir Touili, Anca Muscholl, Ahmed Bouajjani

Publication date: 20 February 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2005.11.007

zbMATH Keywords

verificationrewrite systemsregular model checkingsemi-commutations

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (17)

A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols ⋮ Regular languages and partial commutations ⋮ Unnamed Item ⋮ State Complexity of Permutation and the Language Inclusion Problem up to Parikh Equivalence on Alphabetical Pattern Constraints and Partially Ordered NFAs ⋮ Efficiency of automata in semi-commutation verification techniques ⋮ AUTOMATIC VERIFICATION OF DIRECTORY-BASED CONSISTENCY PROTOCOLS WITH GRAPH CONSTRAINTS ⋮ Regular Model Checking using Widening Techniques ⋮ Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism ⋮ A note on partially ordered tree automata ⋮ Complexity of universality and related problems for partially ordered NFAs ⋮ A Robust Class of Regular Languages ⋮ Local testability from words to traces, a suitable definition ⋮ Automatic Verification of Directory-Based Consistency Protocols ⋮ Geometrically closed positive varieties of languages ⋮ Iterating transducers ⋮ The commutative closure of shuffle languages over group languages is regular ⋮ State complexity of permutation and related decision problems on alphabetical pattern constraints

Cites Work

• A stubborn attack on state explosion
• On recognizable subsets of free partially commutative monoids
• Classifying regular events in symbolic logic
• An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
• A partial approach to model checking
• Polynomial closure and unambiguous product
• Regular Model Checking using Widening Techniques
• Symbolic model checking with rich assertional languages
• Reachability analysis of pushdown automata: Application to model-checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Permutation rewriting and algorithmic verification