Abstract
When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property L is a deterministic finite automaton \(\mathcal {M}_L\) that after each finite execution tells whether (1) every possible extension of the execution is in L, or (2) every possible extension is in the complement of L, or neither (1) nor (2) holds. Moreover, L being monitorable means that it is always possible that in some future the monitor reaches (1) or (2). Classical examples for monitorable properties are safety and cosafety properties. On the other hand, deterministic liveness properties like “infinitely many a’s” are not monitorable.
We discuss various monitor constructions with a focus on deterministic \(\omega \)-regular languages. We locate a proper subclass of deterministic \(\omega \)-regular languages but also strictly larger than the subclass of languages which are deterministic and codeterministic; and for this subclass there exist canonical monitors which also accept the language itself.
We also address the problem to decide monitorability in comparison with deciding liveness. The state of the art is as follows. Given a Büchi automaton, it is PSPACE-complete to decide liveness or monitorability. Given an LTL formula, deciding liveness becomes EXPSPACE-complete, but the complexity to decide monitorability remains open.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Angluin, D., Fisman, D.: Learning regular omega languages. In: Auer, P., Clark, A., Zeugmann, T., Zilles, S. (eds.) ALT 2014. LNCS, vol. 8776, pp. 125–139. Springer, Heidelberg (2014)
Basin, D., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62, 15:1–15:45 (2015)
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)
Diekert, V., Gastin, P.: First-order definable languages. In: Flum, J., Grädel, E., Wilke, Th. (eds.) Logic and Automata: History and Perspectives, Texts in Logic and Games, pp. 261–306. Amsterdam University Press (2008)
Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29–41 (2014). Special Issue of ICTAC 2012
Diekert, V., Muscholl, A.: On distributed monitoring of asynchronous systems. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 70–84. Springer, Heidelberg (2012)
Gondi, K., Patel, Y., Sistla, A.P.: Monitoring the full range of \(\omega \)-regular properties of stochastic systems. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 105–119. Springer, Heidelberg (2009)
Hopcroft, J.E., Ulman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Kamp, H.: Tense logic and the theory of linear order. Ph.D. thesis, University of California (1968)
Knuth, D., Morris, J.H., Pratt, V.: Fast pattern matching in strings. SIAM J. Comput. 6, 323–350 (1977)
Kupferman, O., Vardi, G.: On relative and probabilistic finite counterabilty. In: Kreutzer, S. (ed.) Proceedings 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). LIPIcs, vol. 41, Dagstuhl, Germany, pp. 175–192. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Landweber, L.H.: Decision problems for \(\omega \)-automata. Math. Syst. Theory 3(4), 376–384 (1969)
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293–303 (2009)
Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Inf. Comput. 118, 316–326 (1995)
Martugin, P.V.: A series of slowly synchronizing automata with a zero state over a small alphabet. Inf. Comput. 206, 1197–1203 (2008)
Matiyasevich, Y.: Real-time recognition of the inclusion relation. J. Sov. Math. 1, 64–70 (1973). Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akademii Nauk SSSR, vol. 20, pp. 104–114 (1971)
Nitsche, U., Wolper, P.: Relative liveness and behavior abstraction (extended abstract). In: Burns, J.E., Attiya, H. (eds.) Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing (PODS 1997), Santa Barbara, California, USA, 21–24 August 1997, pp. 45–52. ACM (1997)
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)
Rystsov, I.: Reset words for commutative and solvable automata. Theor. Comput. Sci. 172, 273–279 (1997)
Sistla, A.P., Žefran, M., Feng, Y.: Monitorability of stochastic dynamical systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 720–736. Springer, Heidelberg (2011)
Staiger, L.: Reguläre Nullmengen. Elektronische Informationsverarbeitung und Kybernetik 12(6), 307–311 (1976)
Staiger, L.: Finite-state \(\omega \)-languages. J. Comput. Syst. Sci. 27, 434–448 (1983)
Staiger, L., Wagner, K.W.: Automatentheoretische und automatenfreie Charakterisierungen topologischer Klassen regulärer Folgenmengen. Elektronische Informationsverarbeitung und Kybernetik 10, 379–392 (1974)
Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41, 236–268 (2012)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, chap. 4, pp. 133–191. Elsevier Science Publishers B.V., Amsterdam (1990)
Volkov, M.V.: Synchronizing automata and the Cerný conjecture. In: Martín-Vide, C., Otto, F., Fernau, H. (eds.) LATA 2008. LNCS, vol. 5196, pp. 11–27. Springer, Heidelberg (2008)
Wagner, K.W.: On omega-regular sets. Inf. Control 43, 123–177 (1979)
Acknowledgment
The work was done while the first author was visiting LaBRI in the framework of the IdEx Bordeaux Visiting Professors Programme in June 2015. The hospitality of LaBRI and their members is greatly acknowledged.
The authors thank Andreas Bauer who communicated to us (in June 2012) that the complexity of \(\mathrm {LTL}\)-liveness should be regarded as open because published proofs stating PSPACE-completeness were not convincing. We also thank Ludwig Staiger, Gal Vardi, and Mikhail Volkov for helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Diekert, V., Muscholl, A., Walukiewicz, I. (2015). A Note on Monitors and Büchi Automata. In: Leucker, M., Rueda, C., Valencia, F. (eds) Theoretical Aspects of Computing - ICTAC 2015. ICTAC 2015. Lecture Notes in Computer Science(), vol 9399. Springer, Cham. https://doi.org/10.1007/978-3-319-25150-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-25150-9_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25149-3
Online ISBN: 978-3-319-25150-9
eBook Packages: Computer ScienceComputer Science (R0)