4 papers
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…
Games on Graphs: From Logic and Automata to Algorithms
Nathanaël Fijalkow, C. Aiswarya, Guy Avni +22
The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared…
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…
High-Level Message Sequence Charts: Satisfiability and Realizability Revisited
Benedikt Bollig, Marie Fortin, Paul Gastin
Message sequence charts (MSCs) visually represent interactions in distributed systems that communicate through FIFO channels. High-level MSCs (HMSCs) extend MSCs with choice, conca…