Timed recursive state machines: expressiveness and complexity.

*(English)*Zbl 1338.68070Summary: The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs), which consists of an indexed collection of Timed Automata, called components. Each component can invoke other components in a potentially recursive manner. Besides being able to model procedure calls and recursion, TRSMs are equipped with the ability to suspend the evolution of time within a component when another component is invoked and to recover it when control is given back at return time. This mechanism is realized by storing clock valuations into an implicit stack at invocation time and restoring them upon return. Indeed, TRSMs can be related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. The expressiveness and computational properties of the resulting model are analyzed, showing that it can be used to recognize timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case. However, the problem becomes decidable for two meaningful subclasses, called I-TRSM and L-TRSM, obtained by suitably constraining the set of clocks to reset at invocation time and to restore at return time. The considered subclasses are compared with the corresponding EPTAs subclasses through bisimulation of their timed LTSs. The complexity of the reachability problem for L-TRSM and I-TRSM is proved to be EXPTIME-complete and PSPACE-complete, respectively. Moreover, we prove that such classes strictly enhance the expressive power of Timed Automata and of Pushdown Timed Automata, forming a proper hierarchy.

Reviewer: Reviewer (Berlin)

##### MSC:

68Q05 | Models of computation (Turing machines, etc.) (MSC2010) |

68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |

68Q45 | Formal languages and automata |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

##### Keywords:

formal languages; formal models of computing; timed automata; real-time systems; pushdown systems; recursive state machines
PDF
BibTeX
XML
Cite

\textit{M. Benerecetti} and \textit{A. Peron}, Theor. Comput. Sci. 625, 85--124 (2016; Zbl 1338.68070)

Full Text:
DOI

##### References:

[1] | Abdulla, P. A.; Atig, M. F.; Stenman, J., Dense-timed pushdown automata, (Proceedings of the 27th ACM/IEEE Symposium on Logic in Computer Science, (2012)), 35-44 · Zbl 1360.68535 |

[2] | Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235, (1994) · Zbl 0803.68071 |

[3] | Alur, R.; Madhusudan, P., Decision problems for timed automata: a survey, (Proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication and Software System: Real Time, SFM-RT 2004, (2004)), 1-24 · Zbl 1105.68057 |

[4] | Alur, R.; Courcoubetis, C.; Dill, D., Model-checking in dense real-time, Inform. and Comput., 104, 1, 2-34, (1993) · Zbl 0783.68076 |

[5] | Alur, R.; Benedikt, M.; Etessami, K.; Godefroid, P.; Reps, T. W.; Yannakakis, M., Analysis of recursive state machines, ACM Trans. Program. Lang. Syst., 27, 4, 786-818, (2005) |

[6] | Benerecetti, M.; Minopoli, S.; Peron, A., Analysis of timed recursive state machines, (Proceedings of the 17th International Symposium on Temporal Representation and Reasoning, TIME’10, (2010)), 61-68 |

[7] | Bérard, B.; Gastin, P.; Petit, A., On the power of non-observable actions in timed automata, (Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS’96, (1996)), 257-268 · Zbl 1379.68216 |

[8] | Bérard, B.; Petit, A.; Diekert, V.; Gastin, P., Characterization of the expressive power of silent transitions in timed automata, Fund. Inform., 36, 2-3, 145-182, (1998) · Zbl 0930.68077 |

[9] | Bérard, B.; Haddad, S.; Sassolas, M., Interrupt timed automata: verification and expressiveness, Form. Methods Syst. Des., 40, 1, 41-87, (2012) · Zbl 1247.68124 |

[10] | Bouajjani, A.; Echahed, R.; Robbana, R., Verification of context-free timed systems using linear hybrid observers, (Proceedings of the 6th International Conference on Computer Aided Verification, CAV’94, (1994), Springer), 118-131 |

[11] | Bouajjani, A.; Echahed, R.; Habermehl, P., On the verification problem of nonregular properties for nonregular processes, (Proceedings of the 10th ACM/IEEE Symposium on Logic in Computer Science, (1995)), 123-133 |

[12] | Bouajjani, A.; Echahed, R.; Robbana, R., On the automatic verification of systems with continuous variables and unbounded discrete data structures, (Hybrid Systems II, (1995), Springer), 64-85 |

[13] | Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Updatable timed automata, Theoret. Comput. Sci., 321, 2-3, 291-345, (2004) · Zbl 1070.68063 |

[14] | Cassez, F.; Larsen, K. G., The impressive power of stopwatches, (Proceedings of the 11th International Conference on Concurrency Theory, CONCUR’00, (2000)), 138-152 · Zbl 0999.68112 |

[15] | Dang, Z., Pushdown timed automata: a binary reachability characterization and safety verification, Theoret. Comput. Sci., 302, 1-3, 93-121, (2003) · Zbl 1044.68085 |

[16] | Dang, Z.; Bultan, T.; Ibarra, O. H.; Kemmerer, R. A., Past pushdown timed automata and safety verification, Theoret. Comput. Sci., 313, 1, 57-71, (2004) · Zbl 1069.68065 |

[17] | Henzinger, T. A.; Kopke, P. W.; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, J. Comput. System Sci., 57, 1, 94-124, (1998) · Zbl 0920.68091 |

[18] | Larsen, K. G.; Pettersson, P.; Yi, W., Uppaal in a nutshell, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 134-152, (1997) · Zbl 1060.68577 |

[19] | Li, G.; Cai, X.; Ogawa, M.; Yuen, S., Nested timed automata, (Proceedings of the 11th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS’13, (2013)), 168-182 · Zbl 1390.68407 |

[20] | McManis, J.; Varaiya, P., Suspension automata: a decidable class of hybrid automata, (Proceedings of the 6th International Conference on Computer Aided Verification, CAV’94, (1994), Springer), 105-117 |

[21] | Minsky, M. L., Computation: finite and infinite machines, Prentice-Hall Series in Automatic Computation, (1967), Prentice-Hall · Zbl 0195.02402 |

[22] | Trivedi, A.; Wojtczak, D., Recursive timed automata, (Proceedings of the 8th International Symposium Automated Technology for Verification and Analysis, ATVA’10, (2010)), 306-324 · Zbl 1305.68115 |

[23] | Kronos, S. Yovine, A verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 123-133, (1997) · Zbl 1060.68606 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.