Linear-time temporal logic with event freezing functions

MaRDI QIDQ3384172zbMATH OpenFDO

Authors Stefano Tonetta

Publication date 14 December 2021

Full work available at URL https://arxiv.org/abs/1709.02103, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2017.14

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• scientific article; zbMATH DE number 2080056
• A really temporal logic
• scientific article; zbMATH DE number 4119617
• Temporal logics of repeating values

Cites work

• An Expressive Temporal Logic for Real Time
• Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
• Event-clock automata: a determinizable class of timed automata
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1400049 (Why is no real title available?)
• Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
• LTL with the freeze quantifier and register automata
• Memory event clocks
• On the decidability of continuous time specification formalisms
• On the Expressiveness of MTL Variants over Dense Time
• On the expressiveness of TPTL and MTL
• Real-time logics: Complexity and expressiveness
• Requirements Validation for Hybrid Systems
• Specifying message passing and time-critical systems with temporal logic
• The benefits of relaxing punctuality

Cited in

(1)

• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

Describes a project that uses

Uses Software

• OCRA
• HyComp
• nuXmv

This page was built for publication: Linear-time temporal logic with event freezing functions

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