Parametric runtime verification is NP-complete and coNP-complete

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. (C) 2017 Elsevier B.V. All rights reserved.