SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
DOI10.1016/j.ic.2019.104502zbMath1443.68104OpenAlexW2996279850WikidataQ126581553 ScholiaQ126581553MaRDI QIDQ2182731
Alessandro Cimatti, Stefano Tonetta, Marco Roveri, Alberto Griggio, Enrico Magnago
Publication date: 26 May 2020
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2019.104502
metric temporal logicfirst-order linear-time temporal logicSMT-based model checkingtemporal satisfiability
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Temporal logic (03B44)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Specifying message passing and time-critical systems with temporal logic
- Real-time logics: Complexity and expressiveness
- An SMT-based approach to satisfiability checking of MITL
- Event-clock automata: a determinizable class of timed automata
- \textsc{MightyL}: a compositional translation from MITL to timed automata
- On the expressiveness of TPTL and MTL
- LTL with the freeze quantifier and register automata
- Memory Event Clocks
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Requirements Validation for Hybrid Systems
- On the decidability of continuous time specification formalisms
- The benefits of relaxing punctuality
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
- SMT-Based Induction Methods for Timed Systems
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- An Expressive Temporal Logic for Real Time
This page was built for publication: SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
