Rajeev Alur
Abstract
In real-time decision making and runtime monitoring applications, declarative languages are commonly used as they facilitate modular high-level specifications with the compiler guaranteeing evaluation over data streams in an efficient and incremental manner. We introduce the model of Data Transducers to allow modular compilation of queries over streaming data. A data transducer maintains a finite set of data variables and processes a sequence of tagged data values by updating its variables using an allowed set of operations. The model allows unambiguous nondeterminism, exponentially succinct control, and combining values from parallel threads of computation. The semantics of the model immediately suggests an efficient streaming algorithm for evaluation. The expressiveness of data transducers coincides with streamable regular transductions, a robust and streamable class of functions characterized by MSO-definable string-to-DAG transformations with no backward edges. We show that the novel features of data transducers, unlike previously studied transducers, make them as succinct as traditional imperative code for processing data streams, but the structuring of the transition function permits modular compilation. In particular, we show that operations such as parallel composition, union, prefix-sum, and quantitative analogs of combinators for unambiguous parsing, can be implemented by natural and succinct constructions on data transducers. To illustrate the benefits of such modularity in compilation, we define a new language for quantitative monitoring, QRE-Past, that integrates features of past-time temporal logic and quantitative regular expressions. While this combination allows a natural specification of a cardiac arrhythmia detection algorithm in QRE-Past, compilation of QRE-Past specifications into efficient monitors comes for free thanks to succinct constructions on data transducers.
Supplemental Material
- Houssam Abbas, Rajeev Alur, Konstantinos Mamouras, Rahul Mangharam, and Alena Rodionova. 2018. Real-time Decision Policies with Predictable Performance. To appear in the Proceedings of the IEEE, Special Issue on Design Automation for Cyber-Physical Systems (2018).Google Scholar
- Rajeev Alur and Pavol Cerný. 2010. Expressiveness of Streaming String Transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), Vol. 8.Google Scholar
- Rajeev Alur and Loris D’Antoni. 2012. Streaming Tree Transducers. In 39th International Colloquium on Automata, Languages, and Programming (ICALP ’12). Google ScholarDigital Library
- Rajeev Alur, Loris D’Antoni, Jyotirmoy Deshmukh, Mukund Raghothaman, and Yifei Yuan. 2013. Regular Functions and Cost Register Automata. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’13). Google ScholarDigital Library
- Rajeev Alur, Dana Fisman, Konstantinos Mamouras, Mukund Raghothaman, and Caleb Stanford. In submission, 2018. Streamable Regular Transductions. (In submission, 2018). arXiv: arXiv:1807.03865Google Scholar
- Rajeev Alur, Dana Fisman, and Mukund Raghothaman. 2016. Regular programming for quantitative properties of data streams. In Proceedings of the 25th European Symposium on Programming (ESOP ’16). 15–40.Google ScholarDigital Library
- Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford. 2017. Automata-Based Stream Processing. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP ’17).Google Scholar
- Rajeev Alur and Mukund Raghothaman. 2013. Decision Problems for Additive Regular Functions. In Proceedings of the 40th International Colloquium on Automata, Languages, and Programming (ICALP ’13). Google ScholarDigital Library
- Rajeev Alur and Pavol Černý. 2011. Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages (POPL ’11). Google ScholarDigital Library
- Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. 2004. Rule-based runtime verification. In International Workshop on Verification, Model Checking, and Abstract Interpretation.Google ScholarCross Ref
- Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. 2003. The Synchronous Languages 12 Years Later. Proc. IEEE 91, 1 (2003).Google ScholarDigital Library
- Henrik Björklund and Thomas Schwentick. 2010. On Notions of Regularity for Data Languages. Theoretical Computer Science 411, 4 (2010). Google ScholarDigital Library
- Mikołaj Bojańczyk, Laure Daviaud, and Shankara Narayanan Krishna. 2018. Regular and First-Order List Functions. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Google ScholarDigital Library
- Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. 2011. Two-variable Logic on Data Words. ACM Transactions on Computational Logic (TOCL) 12, 4 (2011). Google ScholarDigital Library
- Patricia Bouyer, Antoine Petit, and Denis Thérien. 2003. An algebraic approach to data languages and timed languages. Information and Computation 182, 2 (2003). Google ScholarDigital Library
- Laura Bozzelli and César Sánchez. 2016. Foundations of Boolean stream runtime verification. Theoretical Computer Science 631 (2016). Google ScholarDigital Library
- Ashok K Chandra, Dexter C Kozen, and Larry J Stockmeyer. 1981. Alternation. Journal of the ACM (JACM) 28, 1 (1981). Google ScholarDigital Library
- Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. 2015. Nested Weighted Automata. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’15). Google ScholarDigital Library
- Bruno Courcelle. 1994. Monadic Second-Order Definable Graph Transductions: A Survey. Theoretical Computer Science 126, 1 (1994). 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 12th International Symposium on Temporal Representation and Reasoning (TIME 2005). Google ScholarDigital Library
- Stéphane Demri and Ranko Lazić. 2009. LTL with the Freeze Quantifier and Register Automata. ACM Transactions on Computational Logic (TOCL) 10, 3 (2009). Google ScholarDigital Library
- Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A. Seshia. 2017. Robust online monitoring of signal temporal logic. Formal Methods in System Design 51, 1 (2017). Google ScholarDigital Library
- Manfred Droste, Werner Kuich, and Heiko Vogler (Eds.). 2009. Handbook of Weighted Automata. Google ScholarDigital Library
- Joost Engelfriet and Sebastian Maneth. 1999. Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations. Information and Computation 154, 1 (1999). Google ScholarDigital Library
- Abdelaziz Fellah, Helmut Jürgensen, and Sheng Yu. 1990. Constructions for alternating finite automata. International journal of computer mathematics 35, 1-4 (1990).Google ScholarCross Ref
- Thomas Ferrère, Thomas A. Henzinger, and N. Ege Saraç. 2018. A Theory of Register Monitors. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Google ScholarDigital Library
- Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma. 2002. Collecting statistics over runtime executions. Electronic Notes in Theoretical Computer Science 70, 4 (2002).Google Scholar
- Klaus Havelund and Grigore Roşu. 2004. Efficient monitoring of safety properties. International Journal on Software Tools for Technology Transfer 6, 2 (2004).Google ScholarCross Ref
- Michael Kaminski and Nissim Francez. 1994. Finite-memory Automata. Theoretical Computer Science 134, 2 (1994). Google ScholarDigital Library
- Martin Leucker and Christian Schallhart. 2009. A Brief Account of Runtime Verification. The Journal of Logic and Algebraic Programming 78, 5 (2009). The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07).Google Scholar
- Konstantinos Mamouras, Mukund Raghothaman, Rajeev Alur, Zachary G. Ives, and Sanjeev Khanna. 2017. StreamQRE: Modular Specification and Efficient Evaluation of Quantitative Queries over Streaming Data. In Proceedings of the 38th Conference on Programming Language Design and Implementation (PLDI ’17). Google ScholarDigital Library
- Zohar Manna and Amir Pnueli. 2012. The temporal logic of reactive and concurrent systems: Specification. Springer Science & Business Media.Google Scholar
- Shanmugavelayutham Muthukrishnan. 2005. Data Streams: Algorithms and Applications. Foundations and Trends® in Theoretical Computer Science 1, 2 (2005). Google ScholarDigital Library
- Frank Neven, Thomas Schwentick, and Victor Vianu. 2004. Finite State Machines for Strings over Infinite Alphabets. ACM Transactions on Computational Logic (TOCL) 5, 3 (2004). Google ScholarDigital Library
- Kai Salomaa, Xiuming Wu, and Sheng Yu. 2000. Efficient implementation of regular languages using reversed alternating finite automata. Theoretical Computer Science 231, 1 (2000). Google ScholarDigital Library
- Marcel Paul Schützenberger. 1961. On the Definition of a Family of Automata. Information and control 4, 2 (1961).Google Scholar
- Prasanna Thati and Grigore Roşu. 2005. Monitoring Algorithms for Metric Temporal Logic Specifications. Electronic Notes in Theoretical Computer Science 113 (2005). Proceedings of the Fourth Workshop on Runtime Verification (RV 2004).Google Scholar
- Yifei Yuan, Dong Lin, Ankit Mishra, Sajal Marwaha, Rajeev Alur, and Boon Thau Loo. 2017. Quantitative Network Monitoring with NetQRE. ACM SIGCOMM Conference on Data Communication (2017). Google ScholarDigital Library
- Jan Zdarek and Carsten W. Israel. 2016. Detection and Discrimination of Tachycardia in ICDs Manufactured by St. Jude Medical. Herzschrittmachertherapie + Elektrophysiologie 27, 3 (2016).Google Scholar
Index Terms
- Modular quantitative monitoring
Recommendations
StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationReal-time decision making in emerging IoT applications typically relies on computing quantitative summaries of large data streams in an efficient and incremental manner. To simplify the task of programming the desired logic, we propose StreamQRE, which ...
Quantitative languages
Quantitative generalizations of classical languages, which assign to each word a real number instead of a Boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition weights) to ...
StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data
PLDI '17Real-time decision making in emerging IoT applications typically relies on computing quantitative summaries of large data streams in an efficient and incremental manner. To simplify the task of programming the desired logic, we propose StreamQRE, which ...
Comments