ABSTRACT
The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k ≥ 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety ω-languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines.
- Stål O Aanderaa. 1973. On k-tape versus (k-1)-tape real time computation. IBM Thomas J. Watson Research Division.Google Scholar
- Bowen Alpern and Fred B Schneider. 1985. Defining liveness. Information processing letters 21, 4 (1985), 181--185.Google Scholar
- Rajeev Alur, Loris D'Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. 2013. Regular Functions and Cost Register Automata. In Symposium on Logic in Computer Science (LICS '13). IEEE Computer Society, Washington, DC, USA, 13--22. Google ScholarDigital Library
- Rajeev Alur, Adam Freilich, and Mukund Raghothaman. 2014. Regular Combinators for String Transformations. In Computer Science Logic and Symposium on Logic in Computer Science (CSL-LICS '14). ACM, New York, NY, USA, Article 9, 10 pages. Google ScholarDigital Library
- Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. 2016. Quantitative Monitor Automata. In International Symposium on Static Analysis. 23--38.Google Scholar
- Yu-Fang Chen, Ondřej Lengál, Tony Tan, and Zhilin Wu. 2017. Register automata with linear arithmetic. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on. IEEE, 1--12.Google ScholarCross Ref
- Marcelo d'Amorim and Grigore Roşu. 2005. Efficient Monitoring of ω-Languages. In Computer Aided Verification (Lecture Notes in Computer Science), Vol. 3576. Springer, 364--378. Google ScholarDigital Library
- Ben d'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B Sipma, Sandeep Mehrotra, and Zohar Manna. 2005. LOLA: Runtime monitoring of synchronous systems. In Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on. IEEE, 166--174. Google ScholarDigital Library
- Stéphane Demri. 2006. Linear-time temporal logics with Presburger constraints: an overview. Journal of Applied Non-Classical Logics 16, 3-4 (2006), 311--347.Google ScholarCross Ref
- Stéphane Demri and Ranko Lazić. 2009. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic 10, 3 (2009), 16. Google ScholarDigital Library
- Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2009. Runtime verification of safety-progress properties. In International Workshop on Runtime Verification. Springer, 40--59. Google ScholarDigital Library
- Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. 2011. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design 38, 3 (2011), 223--262. Google ScholarDigital Library
- Alain Finkel, Stefan Göller, and Christoph Haase. 2013. Reachability in register machines with polynomial updates. In International Symposium on Mathematical Foundations of Computer Science. Springer, 409--420.Google ScholarCross Ref
- Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. 1968. Counter machines and counter languages. Mathematical systems theory 2, 3 (1968), 265--283.Google Scholar
- Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. 1970. Time-restricted sequence generation. J. Comput. System Sci. 4, 1 (1970), 50--73. Google ScholarDigital Library
- MCW Geilen. 2001. On the construction of monitors for temporal logic properties. Electronic Notes in Theoretical Computer Science 55, 2 (2001), 181--199.Google ScholarCross Ref
- Dimitra Giannakopoulou and Klaus Havelund. 2001. Automata-based verification of temporal properties on running programs. In Automated Software Engineering. IEEE, 412--416. Google ScholarDigital Library
- Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, and Nikos Tzevelekos. 2013. Runtime verification based on register automata. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 260--276. Google ScholarDigital Library
- Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. 2010. Variable automata over infinite alphabets. In International Conference on Language and Automata Theory and Applications. Springer, 561--572. Google ScholarDigital Library
- J. Hartmanis and R. E. Stearns. 1965. On the Computational Complexity of Algorithms. Trans. Amer. Math. Soc. 117 (1965), 285--306. http://www.jstor.org/stable/1994208Google ScholarCross Ref
- Klaus Havelund, Giles Reger, Daniel Thoma, and Eugen Zălinescu. 2018. Monitoring events that carry data. In Lectures on Runtime Verification. Springer, 61--102.Google Scholar
- Michael Kaminski and Nissim Francez. 1994. Finite-memory automata. Theoretical Computer Science 134, 2 (1994), 329--363. Google ScholarDigital Library
- Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, and Chao Wang. 2017. Shield synthesis. Formal Methods in System Design 51, 2 (2017), 332--361. Google ScholarDigital Library
- Orna Kupferman and Moshe Y Vardi. 2001. Model checking of safety properties. Formal Methods in System Design 19, 3 (2001), 291--314. Google ScholarDigital Library
- Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan. 1999. Runtime assurance based on formal specifications. Departmental Papers (CIS) (1999), 294.Google Scholar
- Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. The Journal of Logic and Algebraic Programming 78, 5 (2009), 293--303.Google ScholarCross Ref
- Zohar Manna and Amir Pnueli. 2012. Temporal verification of reactive systems: safety. Springer Science & Business Media.Google ScholarDigital Library
- Li Ming and Paul MB Vitányi. 1990. Kolmogorov complexity and its applications. In Algorithms and Complexity. Elsevier, 187--254. Google ScholarDigital Library
- Marvin L. Minsky. 1961. Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines. Annals of Mathematics 74, 3 (1961), 437--455. http://www.jstor.org/stable/1970290Google ScholarCross Ref
- Marvin L Minsky. 1967. Computation: finite and infinite machines. Prentice-Hall. Google ScholarDigital Library
- Wolfgang J. Paul, Joel I. Seiferas, and Janos Simon. 1981. An information-theoretic approach to time bounds for on-line computation. J. Comput. System Sci. 23, 2 (1981), 108--126.Google ScholarCross Ref
- Richard Pollack and M-F Roy. 1993. On the number of cells defined by a set of polynomials. Comptes rendus de l'Académie des sciences. Série 1, Mathématique 316, 6 (1993), 573--577.Google Scholar
- Michael O. Rabin. 1963. Real time computation. Israel Journal of Mathematics 1, 4 (01 Dec 1963), 203--211.Google ScholarCross Ref
- Giles Reger, Helena Cuenca Cruz, and David Rydeheard. 2015. MarQ: monitoring at runtime with QEA. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 596--610. Google ScholarDigital Library
- Arnold L. Rosenberg. 1967. Real-Time Definable Languages. J. ACM 14, 4 (1967), 645--662. Google ScholarDigital Library
- Rich Schroeppel. 1972. A two counter machine cannot calculate 2. Technical Report. MIT.Google Scholar
- Joel I Seiferas and Paul Vitányi. 1988. Counting is easy. Journal of the ACM (JACM) 35, 4 (1988), 985--1000. Google ScholarDigital Library
- J. C. Shepherdson and H. E. Sturgis. 1963. Computability of Recursive Functions. J. ACM 10, 2 (April 1963), 217--255. Google ScholarDigital Library
- Wolfgang Thomas. 1997. Languages, automata, and logic. In Handbook of formal languages. Springer, 389--455. Google ScholarDigital Library
- Moshe Y Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society, 322--331.Google Scholar
- H. Yamada. 1962. Real-Time Computation and Recursive Functions Not Real-Time Computable. IRE Transactions on Electronic Computers EC-11, 6 (Dec 1962), 753--760.Google ScholarCross Ref
- Yifei Yuan, Dong Lin, Ankit Mishra, Sajal Marwaha, Rajeev Alur, and Boon Thau Loo. 2017. Quantitative Network Monitoring with NetQRE. In Conference of the ACM Special Interest Group on Data Communication. ACM, 99--112. Google ScholarDigital Library
Index Terms
- A Theory of Register Monitors
Recommendations
Virtual register renaming
ARCS'13: Proceedings of the 26th international conference on Architecture of Computing SystemsThis paper presents a novel high performance substrate for building energy-efficient out-of-order superscalar cores. The architecture does not require a reorder buffer or physical registers for register renaming and instruction retirement. Instead, it ...
Register write specialization register read specialization: a path to complexity-effective wide-issue superscalar processors
MICRO 35: Proceedings of the 35th annual ACM/IEEE international symposium on MicroarchitectureWith the continuous shrinking of transistor size, processor designers are facing new difficulties to achieve high clock frequency. The register file read time, the wake up and selection logic traversal delay and the bypass network transit delay with ...
Virtual register renaming: energy efficient substrate for continual flow pipelines
GLSVLSI '13: Proceedings of the 23rd ACM international conference on Great lakes symposium on VLSIContinual Flow Pipelines (CFP) allow a processor core to process instruction windows of hundreds of in-flight instructions while keeping its cycle critical scheduler and register file small. CFP defers the execution of instructions that depend on cache ...
Comments