Axiomatizing recursion-free, regular monitors

DOI10.1016/j.jlamp.2022.100778OpenAlexW4224995721MaRDI QIDQ2141297

Luca Aceto, Anna Ingólfsdóttir, Elli Anastasiadi, Antonis Achilleos

Publication date: 25 May 2022

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2006.05463

zbMATH Keywords

process algebraequational logicformal verificationaxiomatizationmonitorsverdict equivalence

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• mCRL2
• JPAX

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The ins and outs of first-order runtime verification
• On finite alphabets and infinite bases
• A complete inference system for a class of regular behaviours
• Partial evaluation and \(\omega\)-completeness of algebraic specifications
• A calculus of communicating systems
• CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
• On a question of A. Salomaa The equational theory of regular expressions over a singleton alphabet is not finitely based
• A completeness theorem for Kleene algebras and the algebra of regular events
• Fundamental approaches to software engineering. 24th international conference, FASE 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 -- April 1, 2021. Proceedings
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• Left-handed completeness
• A brief account of runtime verification
• Monitorability for the Hennessy-Milner logic with recursion
• Optimized temporal monitors for SystemcC
• Rule Systems for Run-time Monitoring: from EAGLE to RULER
• Process algebra for synchronous communication
• Laws of programming
• Algebraic laws for nondeterminism and concurrency
• A term model for synchronous processes
• Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors
• A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
• An Overview of the mCRL2 Toolset and Its Recent Advances
• On finite monoids having only trivial subgroups
• Two Complete Axiom Systems for the Algebra of Regular Events
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Verification, Model Checking, and Abstract Interpretation
• Introduction to the special issue on runtime verification
• Refining the safety-liveness classification of temporal properties according to monitorability

This page was built for publication: Axiomatizing recursion-free, regular monitors