35 citations · 83 across the 19 of their papers we have counts for
24 papers
A Simple Obligation to Metric Interval Temporal Logic
Patricia Bouyer, B Srivathsan, Vaishnavi Vishwanath
Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, ba…
A Zielonka-type Construction for Connectedly Communicating Processes
Béatrice Bérard, Benjamin Monmege, B Srivathsan +1
Given a global specification as a trace-closed regular language, Zielonka's theorem provides a construction to synthesise a language equivalent distributed implementation represent…
Verifying Sequential Consistency under Bounded Preemptions
R. Govind, S. Krishna, Sanchari Sil +1
Gibbons and Korach studied a fundamental problem in 1997: given an observed sequence of reads and writes of a multi-threaded program, does there exist an interleaving which is sequ…
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…
Synthesising Asynchronous Automata from Fair Specifications
Béatrice Bérard, Benjamin Monmege, B Srivathsan +1
Asynchronous automata are a model of distributed finite state processes synchronising on shared actions. A celebrated result by Zielonka shows how a deterministic asynchronous auto…
Model-checking real-time systems: revisiting the alternating automaton route
Patricia Bouyer, B Srivathsan, Vaishnavi Vishwanath
Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logic…
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…
A Local-Time Semantics for Negotiations
Madhavan Mukund, Adwitee Roy, B Srivathsan
Negotiations, introduced by Esparza et al., are a model for concurrent systems where computations involving a set of agents are described in terms of their interactions. In many si…
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…
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…
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…
A Bridge between Polynomial Optimization and Games with Imperfect Recall
Hugo Gimbert, Soumyajit Paul, B. Srivathsan
We provide several positive and negative complexity results for solving games with imperfect recall. Using a one-to-one correspondence between these games on one side and multivari…
Revisiting local time semantics for networks of timed automata
R. Govind, Frédéric Herbreteau, B. Srivathsan +1
We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks…
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…
Reachability in timed automata with diagonal constraints
Paul Gastin, Sayan Mukherjee, B Srivathsan
We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enu…
Nesting Depth of Operators in Graph Database Queries: Expressiveness Vs. Evaluation Complexity
M. Praveen, B. Srivathsan
Designing query languages for graph structured data is an active field of research, where expressiveness and efficient algorithms for query evaluation are conflicting goals. To bet…
Defining relations on graphs: how hard is it in the presence of node partitions?
M. Praveen, B. Srivathsan
Designing query languages for graph structured data is an active field of research. Evaluating a query on a graph results in a relation on the set of its nodes. In other words, a q…
Fast detection of cycles in timed automata
Aakash Deshpande, Frédéric Herbreteau, B. Srivathsan +2
We propose a new efficient algorithm for detecting if a cycle in a timed automaton can be iterated infinitely often. Existing methods for this problem have a complexity which is ex…
Lazy abstractions for timed automata
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency…
Using non-convex approximations for efficient analysis of timed automata
Frédéric Herbreteau, Dileep Kini, B. Srivathsan +1
The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone g…
Better abstractions for timed automata
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstracti…
Coarse abstractions make Zeno behaviours difficult to detect
Frédéric Herbreteau, B Srivathsan
An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find…
Efficient Emptiness Check for Timed Büchi Automata (Extended version)
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
The Büchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solut…