Superposition as a decision procedure for timed automata

DOI10.1007/S11786-012-0134-5zbMath1262.68159OpenAlexW2076908710MaRDI QIDQ1949086

Arnaud Fietzke, Christoph Weidenbach

Publication date: 25 April 2013

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-012-0134-5

zbMATH Keywords

timed automatasuperpositiondecision procedureshierarchic theorem proving

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Related Items (9)

Horn Clause Solvers for Program Verification ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ Superposition for Bounded Domains ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ A complete and terminating approach to linear integer solving ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ On interpolation in automated theorem proving

Uses Software

• Uppaal
• YAGO
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• A theory of timed automata
• Symbolic model checking for real-time systems
• Refutational theorem proving for hierarchic first-order theories
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Solving SAT and SAT Modulo Theories
• Superposition for Fixed Domains
• Engineering DPLL(T) + Saturation
• Integrating Linear Arithmetic into Superposition Calculus
• Superposition Modulo Linear Arithmetic SUP(LA)
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Superposition-Based Analysis of First-Order Probabilistic Timed Automata
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• New results on rewrite-based satisfiability procedures
• Automated Deduction – CADE-20
• Formal Methods for the Design of Real-Time Systems
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Lectures on Concurrency and Petri Nets
• On the Saturation of YAGO
• Formal Modeling and Analysis of Timed Systems

This page was built for publication: Superposition as a decision procedure for timed automata