×

On clock-aware LTL parameter synthesis of timed automata. (English) Zbl 1395.68164

Summary: The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique.

MSC:

68Q45 Formal languages and automata
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

LTL2BA; PPL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (1999), The MIT Press
[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.; Courcoubetis, C.; Dill, D. L., Model-checking for real-time systems, (Proceedings of the Fifth Annual Symposium on Logic in Computer Science, LICS ’90, (1990), IEEE Computer Society), 414-425
[4] Daws, C.; Tripakis, S., Model checking of real-time reachability properties using abstractions, (Tools and Algorithms for Construction and Analysis of Systems, LNCS, vol. 1384, (1998), Springer), 313-329
[5] Behrmann, G.; David, A.; Larsen, K. G.; Håkansson, J.; Pettersson, P.; Yi, W.; Hendriks, M., Uppaal 4.0, (Third International Conference on the Quantitative Evaluation of Systems, QEST 2006, (2006), IEEE), 125-126
[6] Alur, R.; Henzinger, T. A.; Vardi, M. Y., Parametric real-time reasoning, (Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, ACM, (1993)), 592-601 · Zbl 1310.68139
[7] Miller, J. S., Decidability and complexity results for timed automata and semi-linear hybrid automata, (Hybrid Systems: Computation and Control, LNCS, vol. 1790, (2000), Springer), 296-309 · Zbl 0992.93050
[8] Beneš, N.; Bezděk, P.; Larsen, K. G.; Srba, J., Language emptiness of continuous-time parametric timed automata, (International Colloquium on Automata, Languages, and Programming, LNCS, vol. 9135, (2015), Springer), 69-81 · Zbl 1440.68150
[9] Hune, T.; Romijn, J.; Stoelinga, M.; Vaandrager, F. W., Linear parametric model checking of timed automata, J. Log. Algebraic Program., 52-53, 183-220, (2002) · Zbl 1008.68069
[10] Bozzelli, L.; La Torre, S., Decision problems for lower/upper bound parametric timed automata, Form. Methods Syst. Des., 35, 2, 121-151, (2009) · Zbl 1186.68245
[11] Jovanović, A.; Lime, D.; Roux, O. H., Integer parameter synthesis for real-time systems, IEEE Trans. Softw. Eng., 41, 5, 445-461, (2015)
[12] Bezděk, P.; Beneš, N.; Havel, V.; Barnat, J.; Černá, I., On clock-aware LTL properties of timed automata, (Theoretical Aspects of Computing, ICTAC 2014, LNCS, vol. 8687, (2014), Springer), 43-60 · Zbl 1432.68256
[13] André, É.; Chatain, T.; Fribourg, L.; Encrenaz, E., An inverse method for parametric timed automata, Int. J. Found. Comput. Sci., 20, 5, 819-836, (2009) · Zbl 1187.68286
[14] Alur, R.; Henzinger, T. A., A really temporal logic, J. ACM, 41, 1, 181-204, (1994) · Zbl 0807.68065
[15] Koymans, R., Specifying real-time properties with metric temporal logic, Real-Time Syst., 2, 4, 255-299, (1990)
[16] Alur, R.; Feder, T.; Henzinger, T. A., The benefits of relaxing punctuality, J. ACM, 43, 1, 116-146, (1996) · Zbl 0882.68021
[17] Ostroff, J. S., Temporal logic for real-time systems, Research Studies Press Advanced Software Development Series, vol. 40, (1989)
[18] Harel, E.; Lichtenstein, O.; Pnueli, A., Explicit clock temporal logic, (Proceedings of the Fifth Annual Symposium on Logic in Computer Science, LICS ’90, (1990)), 402-413
[19] Demri, S.; D’Souza, D., An automata-theoretic approach to constraint LTL, Inf. Comput., 205, 3, 380-415, (2007) · Zbl 1113.03015
[20] Li, G.; Tang, Z., Modelling real-time systems with continuous-time temporal logic, (Formal Methods and Software Engineering, LNCS, vol. 2495, (2002), Springer), 231-236 · Zbl 1015.68723
[21] Alur, R.; Madhusudan, P., Decision problems for timed automata: a survey, (Formal Methods for the Design of Real-Time Systems, LNCS, vol. 3185, (2004), Springer), 1-24 · Zbl 1105.68057
[22] Baier, C.; Katoen, J.-P., Principles of model checking, (2008), The MIT Press · Zbl 1179.68076
[23] Bezděk, P.; Beneš, N.; Barnat, J.; Černá, I., LTL parameter synthesis of parametric timed automata, (Software Engineering and Formal Methods, LNCS, vol. 9763, (2016), Springer), 172-187 · Zbl 1390.68422
[24] Tripakis, S., Checking timed Büchi automata emptiness on simulation graphs, ACM Trans. Comput. Log., 10, 3, 15, (2009) · Zbl 1352.68165
[25] Dill, D. L., Timing assumptions and verification of finite-state concurrent systems, (Automatic Verification Methods for Finite State Systems, LNCS, vol. 407, (1990), Springer), 197-212
[26] Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, (Lectures on Concurrency and Petri Nets, LNCS, vol. 3098, (2004), Springer), 87-124 · Zbl 1088.68119
[27] P. Pettersson, Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice, Department of Computer Systems, Uppsala University, 1999.; P. Pettersson, Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice, Department of Computer Systems, Uppsala University, 1999.
[28] Bouyer, P., Forward analysis of updatable timed automata, Form. Methods Syst. Des., 24, 3, 281-320, (2004) · Zbl 1073.68041
[29] Lamport, L., What good is temporal logic?, (IFIP Congress, vol. 83, (1983)), 657-668
[30] Tripakis, S.; Yovine, S.; Bouajjani, A., Checking timed Büchi automata emptiness efficiently, Form. Methods Syst. Des., 26, 3, 267-292, (2005) · Zbl 1085.68083
[31] Behrmann, G.; Bouyer, P.; Larsen, K. G.; Pelánek, R., Lower and upper bounds in zone-based abstractions of timed automata, Int. J. Softw. Tools Technol. Transf., 8, 3, 204-215, (2006)
[32] Courcoubetis, C.; Vardi, M. Y.; Wolper, P.; Yannakakis, M., Memory-efficient algorithms for the verification of temporal properties, Form. Methods Syst. Des., 1, 2/3, 275-288, (1992)
[33] Bezděk, P.; Beneš, N.; Černá, I., Bounded parameter synthesis proof-of-concept tool for parametric timed automata, (2018)
[34] Bagnara, R.; Hill, P. M.; Zaffanella, E., The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 1-2, 3-21, (2008)
[35] Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Computer Aided Verification, 13th International Conference, CAV 2001, LNCS, vol. 2102, (2001), Springer), 53-65 · Zbl 0991.68044
[36] Li, G., Checking timed Büchi automata emptiness using LU-abstractions, (Ouaknine, J.; Vaandrager, F. W., Formal Modeling and Analysis of Timed Systems, LNCS, vol. 5813, (2009), Springer), 228-242 · Zbl 1262.68093
[37] Herbreteau, F.; Srivathsan, B.; Walukiewicz, I., Efficient emptiness check for timed Büchi automata, Form. Methods Syst. Des., 40, 2, 122-146, (2012) · Zbl 1247.68143
[38] Tripakis, S.; Yovine, S., Analysis of timed systems using time-abstracting bisimulations, Form. Methods Syst. Des., 18, 1, 25-68, (2001) · Zbl 0971.68096
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.