Verification of Flat FIFO Systems

DOI10.4230/LIPICS.CONCUR.2019.12MaRDI QIDQ5875373zbMATH OpenOpenAlexFDO

Authors M. Praveen, Alain Finkel

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPIcs.CONCUR.2019.12

zbMATH Keywords

complexityreachabilityterminationFIFOcountersinfinite state systemsflat systems

Mathematics Subject Classification ID

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

Recommendations

• Verification of flat FIFO systems
• Verification of Communication Protocols Using Abstract Interpretation of FIFO Queues
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Verification of parametric concurrent systems with prioritized FIFO resource management.
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Reachability problems in piecewise FIFO systems
• Automated verification of automata communicating via FIFO and bag buffers
• scientific article; zbMATH DE number 2086244
• Verification of concurrent systems with VerCors

Cites work

• scientific article; zbMATH DE number 5286864 (Why is no real title available?)
• scientific article; zbMATH DE number 1232238 (Why is no real title available?)
• scientific article; zbMATH DE number 1796145 (Why is no real title available?)
• A perfect model for bounded verification
• Automated Technology for Verification and Analysis
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Forward analysis for WSTS. II: Complete WSTS
• How hard is it to verify flat affine counter systems with the finite monoid property?
• Model-Checking Counting Temporal Logics on Flat Structures
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• On Communicating Finite-State Machines
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Safety problems are NP-complete for flat integer programs with octagonal loops
• Structurally cyclic Petri nets
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• Taming past LTL and flat counter systems
• Testing for unboundedness of fifo channels
• Towards a Model-Checker for Counter Systems
• Using forward reachability analysis for verification of lossy channel systems
• Verification of programs with half-duplex communication
• Well-abstracted transition systems: Application to FIFO automata.

Cited in

(3)

• Verification of flat FIFO systems
• Decidability of membership problems for flat rational subsets of \(\mathrm{GL}(2,\mathbb{Q})\) and singular matrices
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms

Describes a project that uses

Uses Software

• FAST
• Easychair
• FLATA

This page was built for publication: Verification of Flat FIFO Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875373)