Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations

DOI10.1016/S0304-3975(99)00033-XzbMath0933.68089MaRDI QIDQ1960526

Ahmed Bouajjani, Peter Habermehl

Publication date: 12 January 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

verificationautomatalinear constraintsinfinite-state systemssymbolic reachability analysisFIFO-channel systemsnon-regular sets

Mathematics Subject Classification ID

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

Related Items

Reachability problems on reliable and lossy queue automata ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ On iterating linear transformations over recognizable sets of integers ⋮ Model-checking CTL* over flat Presburger counter systems ⋮ Undecidable problems in unreliable computations. ⋮ Verification of Flat FIFO Systems ⋮ Verifying quantitative temporal properties of procedural programs ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES ⋮ A Kleene theorem and model checking algorithms for existentially bounded communicating automata ⋮ LTL over integer periodicity constraints ⋮ Abstract Interpretation of FIFO Replacement ⋮ Unnamed Item ⋮ UNAMBIGUOUS CONSTRAINED AUTOMATA ⋮ BOUNDED PARIKH AUTOMATA ⋮ Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations ⋮ Verification of programs with half-duplex communication ⋮ Flat Petri nets (invited talk) ⋮ Automated analysis of fault-tolerance in distributed systems

Cites Work

• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Testing for unboundedness of fifo channels
• A theory of timed automata
• Unreliable channels are easier to verify than perfect channels
• Verifying programs with unreliable channels
• On Communicating Finite-State Machines
• Reachability analysis of pushdown automata: Application to model-checking