Found 2 Possible Name Variants:

Document

**Published in:** LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline.
Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency.
In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2022.12, author = {Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor}, title = {{Checking Timed B\"{u}chi Automata Emptiness Using the Local-Time Semantics}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {12:1--12:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.12}, URN = {urn:nbn:de:0030-drops-170756}, doi = {10.4230/LIPIcs.CONCUR.2022.12}, annote = {Keywords: Timed B\"{u}chi automata, local-time semantics, zones, abstraction, partial-order reduction} }

Document

**Published in:** LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations.
In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13, author = {Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.}, title = {{Simulations for Event-Clock Automata}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.13}, URN = {urn:nbn:de:0030-drops-170766}, doi = {10.4230/LIPIcs.CONCUR.2022.13}, annote = {Keywords: Event-clock automata, verification, zones, simulations, reachability} }

Document

**Published in:** LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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 of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone.
We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm.

R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting Local Time Semantics for Networks of Timed Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{govind_et_al:LIPIcs.CONCUR.2019.16, author = {Govind, R. and Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor}, title = {{Revisiting Local Time Semantics for Networks of Timed Automata}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {16:1--16:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.16}, URN = {urn:nbn:de:0030-drops-109184}, doi = {10.4230/LIPIcs.CONCUR.2019.16}, annote = {Keywords: Timed automata, verification, local-time semantics, abstraction} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

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 enumerating reachable sets of its configurations, stored in a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.

Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in Timed Automata with Diagonal Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gastin_et_al:LIPIcs.CONCUR.2018.28, author = {Gastin, Paul and Mukherjee, Sayan and Srivathsan, B.}, title = {{Reachability in Timed Automata with Diagonal Constraints}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {28:1--28:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.28}, URN = {urn:nbn:de:0030-drops-95660}, doi = {10.4230/LIPIcs.CONCUR.2018.28}, annote = {Keywords: Timed Automata, Reachability, Zones, Diagonal constraints} }

Document

**Published in:** LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

The liveness problem for timed automata asks if a given automaton has a run passing infinitely often through an accepting state. We show that unless P=NP, the liveness problem is more difficult than the reachability problem; more precisely, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is NP-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with the existing solutions.

Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why Liveness for Timed Automata Is Hard, and What We Can Do About It. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.FSTTCS.2016.48, author = {Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Tran, Thanh-Tung and Walukiewicz, Igor}, title = {{Why Liveness for Timed Automata Is Hard, and What We Can Do About It}}, booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)}, pages = {48:1--48:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-027-9}, ISSN = {1868-8969}, year = {2016}, volume = {65}, editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.48}, URN = {urn:nbn:de:0030-drops-68831}, doi = {10.4230/LIPIcs.FSTTCS.2016.48}, annote = {Keywords: Timed automata, model-checking, liveness invariant, state subsumption} }

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

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 better handle dynamically changing data, recent work has been done on designing query languages that can compare values stored in the graph database, without hard coding the values in the query. The main idea is to allow variables in the query and bind the variables to values when evaluating the query. For query languages that bind variables only once, query evaluation is usually NP-complete. There are query languages that allow binding inside the scope of Kleene star operators, which can themselves be in the scope of bindings and so on. Uncontrolled nesting of binding and iteration within one another results in query evaluation being PSPACE-complete.
We define a way to syntactically control the nesting depth of iterated bindings, and study how this affects expressiveness and efficiency of query evaluation. The result is an infinite, syntactically defined hierarchy of expressions. We prove that the corresponding language hierarchy is strict.
Given an expression in the hierarchy, we prove that it is undecidable to check if there is a language equivalent expression at lower levels. We prove that evaluating a query based on an expression at level i can be done in level i of the polynomial time hierarchy. Satisfiability of quantified Boolean formulas can be reduced to query evaluation; we study the relationship between alternations in Boolean quantifiers and the depth of nesting of iterated bindings.

M. Praveen and B. Srivathsan. Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 117:1-117:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{praveen_et_al:LIPIcs.ICALP.2016.117, author = {Praveen, M. and Srivathsan, B.}, title = {{Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {117:1--117:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.117}, URN = {urn:nbn:de:0030-drops-62520}, doi = {10.4230/LIPIcs.ICALP.2016.117}, annote = {Keywords: graphs with data, regular data path queries, expressiveness, query evaluation, complexity} }

Document

**Published in:** LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

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 graph of the
automaton, which in principle could be infinite. In order to make
the graph finite, zones are approximated using an extrapolation
operator. For reasons of efficiency in current algorithms
extrapolation of a zone is always a zone; and in particular it
is convex.
In this paper, we propose to solve the reachability problem without
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the so
called region closure of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.
An additional benefit of the proposed approach is that it permits to
calculate approximating parameters on-the-fly during exploration of
the zone graph, as opposed to the current methods which do it by a
static analysis of the automaton prior to the exploration. This
allows for further improvements in the algorithm. Promising
experimental results are presented.

Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 78-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.FSTTCS.2011.78, author = {Herbreteau, Fr\'{e}d\'{e}ric and Kini, Dileep and Srivathsan, B. and Walukiewicz, Igor}, title = {{Using non-convex approximations for efficient analysis of timed automata}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)}, pages = {78--89}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-34-7}, ISSN = {1868-8969}, year = {2011}, volume = {13}, editor = {Chakraborty, Supratik and Kumar, Amit}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.78}, URN = {urn:nbn:de:0030-drops-33619}, doi = {10.4230/LIPIcs.FSTTCS.2011.78}, annote = {Keywords: Timed Automata, Model-checking, Non-convex abstraction, On-the-fly abstraction} }

Document

**Published in:** LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Updatable timed automata (UTA) are extensions of classical timed automata that allow special updates to clock variables, like x: = x - 1, x : = y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.

Paul Gastin, Sayan Mukherjee, and B Srivathsan. Reachability for Updatable Timed Automata Made Faster and More Effective. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gastin_et_al:LIPIcs.FSTTCS.2020.47, author = {Gastin, Paul and Mukherjee, Sayan and Srivathsan, B}, title = {{Reachability for Updatable Timed Automata Made Faster and More Effective}}, booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}, pages = {47:1--47:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-174-0}, ISSN = {1868-8969}, year = {2020}, volume = {182}, editor = {Saxena, Nitin and Simon, Sunil}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.47}, URN = {urn:nbn:de:0030-drops-132881}, doi = {10.4230/LIPIcs.FSTTCS.2020.47}, annote = {Keywords: Updatable timed automata, Reachability, Zones, Simulations, Static analysis} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail