Verification of flat FIFO systems

MaRDI QIDQ5129947zbMATH OpenFDO

Authors M. Praveen, Alain Finkel

Publication date 3 November 2020

Full work available at URL https://arxiv.org/abs/1908.07282, https://lmcs.episciences.org/6839

zbMATH Keywords

complexitycountersFIFOflat machinesinfinite state machinesreachabilitytermination

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Verification of Flat FIFO Systems
• scientific article; zbMATH DE number 7471708
• VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES
• Verifying programs with unreliable channels
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,

Cites work

• A perfect model for bounded verification
• Automated Technology for Verification and Analysis
• Complexity hierarchies beyond elementary
• Forward analysis for WSTS. II: Complete WSTS
• How hard is it to verify flat affine counter systems with the finite monoid property?
• scientific article; zbMATH DE number 1696890 (Why is no real title available?)
• 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?)
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Model-Checking Counting Temporal Logics on Flat Structures
• On Communicating Finite-State Machines
• On the complexity of integer programming
• 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

(6)

• Branch-well-structured transition systems and extensions
• scientific article; zbMATH DE number 7471708 (Why is no real title available?)
• Verification of Flat FIFO Systems
• On the preservation of properties when changing communication models
• Branch-well-structured transition systems and extensions
• Reachability problems on reliable and lossy queue automata

Describes a project that uses

Uses Software

• TREX
• FLATA
• FAST

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 Q5129947)