Parametric runtime verification is NP-complete and coNP-complete. (English) Zbl 1405.68181
Summary: In this article, we solve an important open problem - the computational complexity of parametric runtime verification against regular properties. To achieve this, we first formulate the membership problem of existential and universal parametric languages, then show that the membership problem of existential parametric regular languages is NP-complete, and the membership problem of universal parametric regular languages is coNP-complete. These computational complexity results show that parametric runtime verification of regular properties is NP-complete and coNP-complete. This gives a rigorous proof and a formal explanation of the inherent intractability of parametric runtime verification, which has been shown by the empirical experiments in the literature. In this sense, our work has moved one significant step on the theoretical aspect of runtime monitoring and verification.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q45 | Formal languages and automata |
Keywords:
runtime monitoring; computational complexity; formal languages; parametric words; membership problemsReferences:
| [1] | Chen, Z.; Wang, Z.; Zhu, Y.; Xi, H.; Yang, Z., Parametric runtime verification of C programs, (Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016, Lecture Notes in Computer Science, vol. 9636 (2016), Springer), 299-315 |
| [2] | Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebraic Program., 78, 293-303 (2009) · Zbl 1192.68433 |
| [3] | Allan, C.; Avgustinov, P.; Christensen, A. S.; Hendren, L. J.; Kuzins, S.; Lhoták, O.; de Moor, O.; Sereni, D.; Sittampalam, G.; Tibble, J., Adding trace matching with free variables to AspectJ, (Johnson, R. E.; Gabriel, R. P., Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005 (2005), ACM), 345-364 |
| [4] | Avgustinov, P.; Tibble, J.; de Moor, O., Making trace monitors feasible, (Gabriel, R. P.; Bacon, D. F.; Lopes, C. V.; Steele, J. Guy L., Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007 (2007), ACM), 589-608 |
| [5] | Chen, F.; Rosu, G., MOP: an efficient and generic runtime verification framework, (Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007 (2007), ACM), 569-588 |
| [6] | Rosu, G.; Chen, F., Semantics and algorithms for parametric monitoring, Log. Methods Comput. Sci., 8, 1-47 (2012) · Zbl 1237.68065 |
| [7] | Hopcroft, J. E.; Ullman, J. D., Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading MA · Zbl 0196.01701 |
| [8] | Holzer, M.; Kutrib, M., Descriptional and computational complexity of finite automata - a survey, Inf. Comput., 209, 456-470 (2011) · Zbl 1217.68130 |
| [9] | Papadimitriou, C. H., Computational Complexity (1994), Addison-Wesley: Addison-Wesley Reading MA · Zbl 0557.68033 |
| [10] | Liu, Y. A.; Rothamel, T.; Yu, F.; Stoller, S. D.; Hu, N., Parametric regular path queries, (Pugh, W.; Chambers, C., Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2004 (2004), ACM), 219-230 |
| [11] | Kurshan, R. P., The complexity of verification, (Leighton, F. T.; Goodrich, M. T., Proceedings of the 26th Annual ACM Symposium on Theory of Computing (1994), ACM), 365-371 · Zbl 1345.68220 |
| [12] | Esparza, J.; Ganty, P., Complexity of pattern-based verification for multithreaded programs, (Ball, T.; Sagiv, M., Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011 (2011), ACM), 499-510 · Zbl 1284.68182 |
| [13] | Esparza, J., Keeping a crowd safe: on the complexity of parameterized verification, (Mayr, E. W.; Portier, N., Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science. Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014. Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science. Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, LIPIcs, vol. 25 (2014), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 1-10 · Zbl 1359.68189 |
| [14] | Bonakdarpour, B.; Navabpour, S.; Fischmeister, S., Sampling-based runtime verification, (Butler, M. J.; Schulte, W., Proceedings of the 17th International Symposium on Formal Methods. Proceedings of the 17th International Symposium on Formal Methods, FM 2011. Proceedings of the 17th International Symposium on Formal Methods. Proceedings of the 17th International Symposium on Formal Methods, FM 2011, Lecture Notes in Computer Science, vol. 6664 (2011), Springer), 88-102 |
| [15] | Bonakdarpour, B.; Thomas, J. J.; Fischmeister, S., Time-triggered program self-monitoring, (Proceedings of the 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications. Proceedings of the 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2012 (2012), IEEE Computer Society), 260-269 |
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.
