Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
From MaRDI portal
Publication:1960526
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)
verificationautomatalinear constraintsinfinite-state systemssymbolic reachability analysisFIFO-channel systemsnon-regular sets
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
