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 (19)

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

This page was built for publication: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations