Well-abstracted transition systems: Application to FIFO automata.

DOI10.1016/S0890-5401(02)00027-5zbMath1054.68092MaRDI QIDQ1401924

S. Purushothaman Iyer, Grégoire Sutre, Alain Finkel

Publication date: 19 August 2003

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

zbMATH Keywords

ProtocolsAccelerationFlatnessAbstractionInfinite state systemsFIFO automataRegular expressionsSymbolic representation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Verification of Flat FIFO Systems ⋮ Acceleration in Convex Data-Flow Analysis ⋮ Unnamed Item ⋮ BOUNDED PARIKH AUTOMATA ⋮ Verification of programs with half-duplex communication

Cites Work

• Testing for unboundedness of fifo channels
• An introduction to FIFO nets - monogeneous nets: a subclass of FIFO nets
• The complexity of logical theories
• Reduction and covering of infinite reachability trees
• Symbolic model checking: \(10^{20}\) states and beyond
• On the equivalence, containment, and covering problems for the regular and context-free languages
• A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
• Parallel program schemata
• On Communicating Finite-State Machines
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• Derivatives of Regular Expressions
• Well-structured transition systems everywhere!
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item