Proving the existence of fair paths in infinite-state systems

DOI10.1007/978-3-030-67067-2_6zbMath1472.68085OpenAlexW3120288634MaRDI QIDQ2234061

Enrico Magnago, Alberto Griggio, Alessandro Cimatti

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Automatic discovery of fair paths in infinite-state transition systems ⋮ Verification Modulo theories ⋮ Iterative bounded synthesis for efficient cycle detection in parametric timed automata ⋮ \textsc{LTL} falsification in infinite-state systems

Cites Work

• Unnamed Item
• A compositional approach to CTL\(^*\) verification
• Geometric nontermination arguments
• Model checking with strong fairness
• Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
• Falsification of temporal properties of hybrid systems using the cross-entropy method
• S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
• Compositional Reasoning
• Proving non-termination
• Proving Termination of Programs Automatically with AProVE
• Falsification of LTL Safety Properties in Hybrid Systems
• Checking Timed Büchi Automata Emptiness Using LU-Abstractions
• “Sometimes” and “not never” revisited
• Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
• SMT-Based Induction Methods for Timed Systems
• Predicate Abstraction with Under-approximation Refinement
• Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>
• Formal Methods for the Design of Real-Time Systems
• Hybrid Systems: Computation and Control
• Termination of triangular Integer loops is decidable

This page was built for publication: Proving the existence of fair paths in infinite-state systems