10 citations · 44 across the 22 of their papers we have counts for
33 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…
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…
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…
Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages
Bharat Adsul, Paul Gastin, Shantanu Kulkarni +1
We propose a local, past-oriented fragment of propositional dynamic logic to reason about concurrent scenarios modelled as Mazurkiewicz traces, and prove it to be expressively comp…
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…
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…
Zone-based verification of timed automata: extrapolations, simulations and what next?
Patricia Bouyer, Paul Gastin, Frédéric Herbreteau +2
Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real…
Simulations for Event-Clock Automata
S Akshay, Paul Gastin, R Govind +1
Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically usef…
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,…
Fast zone-based algorithms for reachability in pushdown timed automata
S. Akshay, Paul Gastin, Karthik R Prakash
Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed auto…
Asynchronous wreath product and cascade decompositions for concurrent behaviours
Bharat Adsul, Paul Gastin, Saptarshi Sarkar +1
We develop new algebraic tools to reason about concurrent behaviours modelled as languages of Mazurkiewicz traces and asynchronous automata. These tools reflect the distributed nat…
SD-Regular Transducer Expressions for Aperiodic Transformations
Luc Dartois, Paul Gastin, Shankara Narayanan Krishna
FO transductions, aperiodic deterministic two-way transducers, as well as aperiodic streaming string transducers are all equivalent models for first order definable functions. In t…
Weighted Tiling Systems for Graphs: Evaluation Complexity
C. Aiswarya, Paul Gastin
We consider weighted tiling systems to represent functions from graphs to a commutative semiring such as the Natural semiring or the Tropical semiring. The system labels the nodes…
Reachability for Updatable Timed Automata made faster and more effective
Paul Gastin, Sayan Mukherjee, B Srivathsan
Updatable timed automata (UTA) are extensions of classic timed automata that allow special updates to clock variables, like x:= x - 1, x := y + 2, etc., on transitions. Reachabilit…
Wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces (extended version)
Bharat Adsul, Paul Gastin, Saptarshi Sarkar +1
We develop a new algebraic framework to reason about languages of Mazurkiewicz traces. This framework supports true concurrency and provides a non-trivial generalization of the wre…
Register transducers are marble transducers
Gaëtan Douéneau-Tabot, Emmanuel Filiot, Paul Gastin
Deterministic two-way transducers define the class of regular functions from words to words. Alur and Cerný introduced an equivalent model of transducers with registers called copy…
Revisiting Underapproximate Reachability for Multipushdown Systems
S. Akshay, Paul Gastin, S Krishna +1
Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in ana…
Modular Descriptions of Regular Functions
Paul Gastin
We discuss various formalisms to describe string-to-string transformations. Many are based on automata and can be seen as operational descriptions, allowing direct implementations…
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…
Timed Systems through the Lens of Logic
S. Akshay, Paul Gastin, Vincent Juge +1
In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using grap…
Fast algorithms for handling diagonal constraints in timed automata
Paul Gastin, Sayan Mukherjee, B Srivathsan
A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as zones. A naïve enumeration of zones does not termina…
Non-Sequential Theory of Distributed Systems
Benedikt Bollig, Paul Gastin
These lecture notes cover basic automata-theoretic concepts and logical formalisms for the modeling and verification of concurrent and distributed systems. Many of these concepts n…
Aperiodic Weighted Automata and Weighted First-Order Logic
Manfred Droste, Paul Gastin
By fundamental results of Schützenberger, McNaughton and Papert from the 1970s, the classes of first-order definable and aperiodic languages coincide. Here, we extend this equivale…
Unambiguous Forest Factorization
Paul Gastin, Shankara Narayanan Krishna
In this paper, we look at an unambiguous version of Simon's forest factorization theorem, a very deep result which has wide connections in algebra, logic and automata. Given a morp…