Distributed Timed Automata with Independently Evolving Clocks

• Autorzy: Akshay S. , Bollig B. , Gastin P. , Mukund M. , Kumar K. N.

Identyfikatory

DOI

10.3233/FI-2014-996

• Języki publikacji: EN

Abstrakty

EN

We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.

Słowa kluczowe

EN

Timed Automata; distributed systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 4
• Strony: 377--407
• Opis fizyczny: Bibliogr. 19 poz., rys., wykr.

Twórcy

autor

Akshay S.

• LSV, ENS Cachan, CNRS, INRIA, France

autor

Bollig B.

• LSV, ENS Cachan, CNRS, INRIA, France

autor

Gastin P.

• LSV, ENS Cachan, CNRS, INRIA, France

autor

Mukund M.

• Chennai Mathematical Institute, Chennai, India

autor

Kumar K. N.

• Chennai Mathematical Institute, Chennai, India

Bibliografia

• [1] Akshay, S., Bollig, B., Gastin, P., Mukund, M., Narayan Kumar, K.: Distributed Timed Automata with Independently Evolving Clocks, Proc. of CONCUR, 5201, Springer, 2008.
• [2] Alur, R., Dill, D. L.: A Theory of Timed Automata., Theoretical Computer Science, 126(2), 1994, 183–235.
• [3] Alur, R., Madhusudan, P.: Decision Problems for Timed Automata: A Survey, Formal Methods for the Design of Real-Time Systems, Springer, 2004.
• [4] Bengtsson, J., Jonsson, B., Lilius, J., Yi,W.: Partial Order Reductions for Timed Systems, Proc. of CONCUR, 1466, Springer, 1998.
• [5] Birget, J.-C.: State-complexity of finite-state devices, state compressibility and incompressibility, Mathematical Systems Theory, 26(3), 1993, 237–269.
• [6] Bouyer, P., Haddad, S., Reynier, P.-A.: Timed Unfoldings for Networks of Timed Automata, Proc. of ATVA, 4218, Springer, 2006.
• [7] Cassez, F., Chatain, T., Jard, C.: Symbolic Unfoldings For Networks of Timed Automata, Proc. of ATVA, 4218, Springer, 2006.
• [8] Cassez, F., Henzinger, T. A., Raskin, J.-F.: A Comparison of Control Problems for Timed and Hybrid Systems, Proc. of HSCC, 2289, Springer, 2002.
• [9] De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and Implementability of Timed Automata, Proc. of FORMATS and FTRTFT, 3253, Springer, 2004.
• [10] Dima, C., Lanotte, R.: Distributed Time-Asynchronous Automata, Proc. of ICTAC, 4711, Springer, 2007.
• [11] Genest, B.: On Implementation of Global Concurrent Systems with Local Asynchronous Controllers., Proc. of CONCUR, 3653, Springer, 2005.
• [12] Henzinger, T. A.: The theory of hybrid automata, Proc. of LICS, IEEE Computer Society, 1996.
• [13] Larsen, K. G., Pettersson, P., Yi, W.: Compositional and symbolic model-checking of real-time systems, Proc. of RTSS, IEEE Computer Society, 1995.
• [14] Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata, Theoretical Computer Science, 345(1), 2005, 27–59.
• [15] Peterson, G., Reif, J.: Multiple-Person Alternation, Proc. of FOCS, 1979.
• [16] Peterson, G., Reif, J., Azhar, S.: Lower Bounds for Multiplayer Noncooperative Games of Incomplete Information, Comput. Math. Appl., 41, 2001, 957–992.
• [17] Puri, A.: Dynamical Properties of Timed Automata, Discrete Event Dynamic Systems, 10(1-2), 2000, 87–113, ISSN 0924-6703.
• [18] Swaminathan, M., Fränzle, M., Katoen, J.-P.: The surprising robustness of (closed) timed automata against clock-drift, Proc. of IFIP-TCS, 273, Springer, 2008.
• [19] Zielonka,W.: Notes on finite asynchronous automata, R.A.I.R.O.— Informatique Théorique et Applications, 21, 1987, 99–135.