6 papers · 1 filter
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
S. Akshay, Prerak Contractor, Paul Gastin +2
Model checking for real-timed systems is a rich and diverse topic. Among the different logics considered, Metric Interval Temporal Logic (MITL) is a powerful and commonly used logi…
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm
S. Akshay, Paul Gastin, R. Govind +1
The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities…
Reversible Transducers over Infinite Words
Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn +2
Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related t…
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
S Akshay, Paul Gastin, R Govind +2
In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including time…
Efficient Construction of Reversible Transducers from Regular Transducer Expressions
Luc Dartois, Paul Gastin, R. Govind +1
The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers,…
Logics for Reversible Regular Languages and Semigroups with Involution
Paul Gastin, Amaldev Manuel, R. Govind
We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse opera…