AVeRTS - Algorithmic Verification of Real-Time Systems
AVeRTS in an Indo-French project on the algorithmic verification of
real-time systems. The project is funded by CNRS on the french side, and
by DST on the Indian side, under the CEFIPRA - Indo-French Program in ICST
2014-2016.


Members
Bordeaux
|
Rennes
|
Chennai
|
Mumbai
|
Frédéric Herbreteau |
Nathalie Bertrand |
B. Srivathsan |
S. Krishna |
Igor Walukiewicz |
Blaise Genest |
|
S. Akshay |
Thanh Tung Tran |
Paulin Fournier |
|
Ashutosh Trivedi |
|
|
|
Devendra Bhave |
Project leaders: Frédéric Herbreteau (LaBRI, France),
S. Krishna (IIT Bombay, India)
Activity
- Blaise Genest (IRISA) is visiting CMI Chennai and IIT Bombay
in January/February 2017.
- Srivathsan B (CMI Chennai) is visiting LaBRI in January
2017.
- 2nd
AVeRTS workshop, satellite event of FSTTCS 2016, CMI
Chennai, December 16th 2016.
- S. Akshay (IIT Bombay) is visiting IRISA in June 2016.
- Workshop:
Trends and Challenges in Quantitative
Verification at Mysore Park, 1-4 Feb. 2016
- 1st AVeRTS workshop, satellite event of FSTTCS 2015, IISc
Bangalore, December 19th 2015.
- Ramanathan Varun (student of CMI Chennai) is an intern at
LaBRI from May to July 2015.
- Ashutosh Trivedi (IIT Bombay) is visiting LaBRI in July
2015.
- S. Akshay (IIT Bombay) is visiting IRISA in June 2015.
- Ravichandra Adanki (student of IIT Bombay) is an intern at
LaBRI from May to July 2015.
- Miheer Dewaskar (student of CMI Chennai) is an intern at
IRISA from May to July 2015.
- Srivathsan B (CMI Chennai) is visiting LaBRI from 5th to
31st of January 2015.
- N. Bertrand (IRISA) is visiting IIT Bombay in December 2014.
- S. Akshay (IIT Bombay) is visiting IRISA in May and June 2014.
- Srivathsan B (CMI Chennai) is visiting LaBRI in May 2014.
- Aakash Deshpande (student of IIT Bombay) is an intern at LaBRI from
5th May to 10th July 2014, working on "Efficient detection of
cycles in timed automata".
Description of the project
Digital systems control most of the devices that surround us. Timing
constraints are often crucial for cyber-physical systems that are designed
to interact with the physical world. Correctness of cyber-physical systems
that work under time-constraints is an ongoing challenge since traditional
methods based on testing are no longer applicable in a safety-critical
setting. This project aims at enlarging the applicability of formal
verification for certifying correctness of timed systems. Formal
verification requires that a system be modeled as a mathematical object.
The model of timed automata has been introduced more than 25 years ago and
has been an object of intensive study. It has also been successfully used
in verification of cyber-physical systems.
The main scientific goal of the project is to enable control designers to
exploit advances in formal verification of time critical cyber-physical
systems. There have been several recent improvements to the existing
state-of-the-art algorithms for verification of timed systems. We believe
that these open up real opportunities to scale formal verification to
larger and more complex systems. We plan to further improve the algorithms
and integrate them in a tool that we are developing. In particular, we
will take into account stochastic and distributed nature of modern
cyber-physical systems. We also aim to apply these techniques to
industrial-level applications.
Related publications by project members
Verification, games and synthesis for timed systems
- Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, Ashutosh
Trivedi: Expected reachability-time
games. Theor. Comput. Sci. 631: 139-160 (2016)
- Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz:
Better abstractions for timed automata. Inf. Comput. 251: 67-90
(2016)
- Shibashis Guha, Marcin Jurdzinski, Shankara Narayanan
Krishna and Ashutosh Trivedi. Mean-Payoff Games on Timed
Automata. FSTTCS 2016: 44:1-44:14.
- F. Herbreteau, B. Srivathsan, T.T. Tran and
I. Walukiewicz. Why liveness for timed automata is hard and what
we can do about it. FSTTCS 2016: 48:1-48:14
- S. Akshay, Paul Gastin, Shankara Narayanan Krishna:
Analyzing Timed Systems Using Tree Automata. CONCUR 2016:
27:1-27:14
- Shibashis Guha, Shankara Narayanan Krishna, Lakshmi Manasa,
Ashutosh Trivedi: Revisiting Robustness in Priced Timed
Games. FSTTCS 2015: 261-277
- Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh
Trivedi: What's decidable about recursive hybrid automata? HSCC
2015: 31-40
- Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh
Trivedi: Time-Bounded Reachability Problem for Recursive Timed
Automata is Undecidable. LATA 2015: 237-248
- Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh
Trivedi: Reachability Games on Recursive Hybrid Automata. TIME
2015: 150-159
- Frédéric Herbreteau, Thanh-Tung Tran: Improving Search Order
for Reachability Testing in Timed Automata. FORMATS 2015:
124-139.
- S. Krishna, Umang Mathur and Ashutosh Trivedi: Weak Singular
Hybrid Automata. FORMATS 2014.
- Bernard Boigelot, Frédéric Herbreteau and
Isabelle Mainz: Acceleration of Hybrid Affine
Transformations. ATVA 2014
- Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Lazy
Abstractions for Timed Automata. CAV 2013: 990-1005
- Frédéric Herbreteau, B. Srivathsan: Coarse abstractions make Zeno
behaviours difficult to detect. Logical Methods in Computer
Science 9(1) (2013)
- Fredéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Efficient
emptiness check for timed Büchi automata. Formal Methods in System
Design 40(2): 122-146 (2012)
- Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Better
Abstractions for Timed Automata. LICS 2012: 375-384
- Frédéric Herbreteau, Dileep Kini, B. Srivathsan, Igor Walukiewicz:
Using non-convex approximations for efficient analysis of timed
automata. FSTTCS 2011: 78-89
Communicating/Distributed timed systems
- S. Akshay, Loïc Hélouët, Claude Jard, Pierre-Alain Reynier:
Robustness of Time Petri Nets under Guard
Enlargement. Fundam. Inform. 143(3-4): 207-234 (2016)
- S. Akshay, Blaise Genest, Loïc Hélouët: Decidable Classes of
Unbounded Petri Nets with Time and Urgency. Petri Nets 2016:
301-322
- S. Akshay, Loïc Hélouët, Ramchandra Phawade:
Combining Free Choice and Time in Petri Nets. TIME 2016: 120-129
- Lorenzo Clemente, Frédéric Herbreteau and
Grégoire Sutre: Decidable Topologies for Communicating
Automata with FIFO and Bag Channels. CONCUR 2014.
- S. Akshay, Benedikt Bollig, Paul Gastin: Event clock message passing
automata: a logical characterization and an emptiness checking
algorithm. Formal Methods in System Design 42(3): 262-300 (2013)
- S. Akshay, Ionut Dinca, Blaise Genest, Alin Stefanescu. Implementing
Realistic Asynchronous Automata. FSTTCS 2013
- Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer and Grégoire
Sutre: Reachability of Communicating Timed Processes. FoSSaCS 2013:
81-96
- S. Akshay, Blaise Genest, Loïc Hélouët, Shaofa Yang: Regular set of
representatives for time-constrained MSC graphs. Inf. Process. Lett.
112(14-15): 592-598 (2012)
- S. Akshay, Blaise Genest, Loïc Hélouët, Shaofa Yang: Symbolically
Bounding the Drift in Time-Constrained MSC Graphs. ICTAC 2012:
1-15
- S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund, K. Narayan
Kumar: Distributed Timed Automata with Independently Evolving Clocks.
CONCUR 2008: 82-97
Verification, games and synthesis for stochastic (timed) systems
- S. Akshay, Blaise Genest, Bruno Karelovic, Nikhil Vyas:
On Regularity of Unary Probabilistic Automata. STACS 2016: 8:1-8:14
- Nathalie Bertrand, Serge Haddad, Engel Lefaucheux:
Diagnosis in Infinite-State Probabilistic Systems. CONCUR 2016:
37:1-37:15
- S. Akshay, Patricia Bouyer, Shankara Narayanan Krishna,
Lakshmi Manasa, Ashutosh Trivedi: Stochastic Timed Games
Revisited. MFCS 2016: 8:1-8:14
- Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Pierre
G. Carlier: Analysing Decisive Stochastic Processes. ICALP 2016:
101:1-101:14
- Nathalie Bertrand, Serge Haddad, Engel Lefaucheux:
Accurate Approximate Diagnosability of Stochastic Systems. LATA 2016:
549-561
- Manindra Agrawal, S. Akshay, Blaise Genest,
P. S. Thiagarajan: Approximate Verification of the Symbolic
Dynamics of Markov Chains. J. ACM 62(1): 2:1-2:34 (2015)
- S. Akshay, Timos Antonopoulos, Joël Ouaknine, James Worrell:
Reachability problems for Markov chains. Inf. Process. Lett. 115(2):
155-158 (2015)
- S. Akshay, Paul Gastin, Madhavan Mukund, K. Narayan Kumar:
Checking conformance for time-constrained scenario-based
specifications. Theor. Comput. Sci. 594: 24-43 (2015)
- Ankush Das, Shankara Narayanan Krishna, Lakshmi Manasa,
Ashutosh Trivedi, Dominik Wojtczak: On Pure Nash Equilibria in
Stochastic Games. TAMC 2015: 359-371
- Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin
Menet, Christel Baier, Marcus Größer, Marcin Jurdzinski:
Stochastic Timed Automata. Logical Methods in Computer Science
10(4) (2014)
- Nathalie Bertrand, Thomas Brihaye and Blaise
Genest: Deciding the value 1 problem for reachability in 1-clock
decision stochastic timed automata. QEST 2014
- S. Krishna, Lakshmi Manasa and Ashutosh Trivedi: Improved
Undecidability Results for Reachability Games on Recursive Timed
Automata. GandALF 2014.
- Thomas Brihaye, Gilles Gerraerts, S. Krishna, Lakshmi
Manasa, Benjamin Monmenge and Ashutosh Trivedi: Adding Negative
Prices to Priced Timed Games. CONCUR 2014.
- S.Akshay, Nathalie Bertrand, Serge Haddad, Loïc Hélouët: The
Steady-State Control Problem for Markov Decision Processes. QEST 2013:
290-304
- S. Krishna, Lakshmi Manasa, Ashish Chiplunkar: Nash Equilibrium in
Weighted Concurrent Timed Games with Reachability Objectives. ICDCIT
2012: 117-128
- Nathalie Bertrand, Sven Schewe: Playing Optimally on Timed Automata
with Random Delays. FORMATS 2012: 43-58
- Rajeev Alur, Ashutosh Trivedi: Relating average and discounted costs
for quantitative analysis of timed systems. EMSOFT 2011:
165-174
- Dileep Kini, S. Krishna, Paritosh K. Pandya: On
Construction of Safety Signal Automata for MITL[U, S] Using
Temporal Projections. FORMATS 2011: 225-239
- Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye,
Marcus Größer: Almost-Sure Model Checking of Infinite Paths in One-Clock
Timed Automata. LICS 2008: 217-226
- Marcin Jurdzinski, Ashutosh Trivedi: Average-Time Games. FSTTCS 2008:
340-351
- Marcin Jurdzinski, Ashutosh Trivedi: Reachability-Time Games on Timed
Automata. ICALP 2007: 838-849
Timed automata, languages and logics
- Shankara Narayanan Krishna, Khushraj Madnani, Paritosh K. Pandya:
Metric Temporal Logic with Counting. FoSSaCS 2016: 335-352
- Devendra Bhave, Vrunda Dave, Shankara Narayanan Krishna,
Ramchandra Phawade, Ashutosh Trivedi: A Perfect Class of
Context-Sensitive Timed Languages. DLT 2016: 38-50
- Devendra Bhave, Vrunda Dave, Shankara Narayanan Krishna,
Ramchandra Phawade, Ashutosh Trivedi: A Logical Characterization
for Dense-Time Visibly Pushdown Automata. LATA 2016: 89-101
- Nathalie Bertrand, Amélie Stainer, Thierry Jéron, Moez Krichen:
A game approach to determinize timed automata. Formal Methods in
System Design 46(1): 42-80 (2015)
- S. Krishna, Khushraj Madnani and Paritosh Pandya: Partially
Punctual Metric Temporal Logic is Decidable. TIME 2014.
- S. Krishna, Krushraj Madnani and Paritosh Pandya: On Unary
Fragments of MTL and TPTL over Timed Words. ICTAC 2014.
- Rajeev Alur, Vojtech Forejt, Salar Moarref, Ashutosh Trivedi: Safe
schedulability of bounded-rate multi-mode systems. HSCC 2013:
243-252
- Pawel Parys, Igor Walukiewicz: Weak Alternating Timed Automata.
Logical Methods in Computer Science 8(3) (2012)
- Rajeev Alur, Ashutosh Trivedi, Dominik Wojtczak: Optimal scheduling
for constant-rate multi-mode systems. HSCC 2012: 75-84
- Lakshmi Manasa, S. Krishna, Chinmay Jain: Model Checking Weighted
Integer Reset Timed Automata. Theory Comput. Syst. 48(3):
648-679 (2011)
- Nathalie Bertrand, Amélie Stainer, Thierry Jéron, Moez
Krichen: A Game Approach to Determinize Timed Automata. FOSSACS
2011: 245-259
- Slawomir Lasota, Igor Walukiewicz: Alternating timed automata. ACM
Trans. Comput. Log. 9(2)