Determinizing monitors for HML with recursion

DOI10.1016/J.JLAMP.2019.100515MaRDI QIDQ2291832zbMATH OpenOpenAlexWikidataFDO

Authors Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingolfsdottir, Sævar Örn Kjartansson

Publication date 31 January 2020

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

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

zbMATH Keywords

Hennessy-Milner logicruntime verificationdeterminizationcomplexity boundsmonitorability

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then they can be exponentially more succinct than their CCS process form.

Recommendations

• On the complexity of determinizing monitors
• Monitorability for the Hennessy-Milner logic with recursion
• A theory of register monitors
• A note on monitors and Büchi automata
• Consistently-detecting monitors

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 7354705 (Why is no real title available?)
• A brief account of runtime verification
• A complete axiomatisation for trace congruence of finite state behaviors
• A framework for parameterized monitorability
• Comparing LTL semantics for runtime verification
• Computer Aided Verification
• Finite automata and unary languages
• Formal verification of parallel programs
• Inapproximability of Nondeterministic State and Transition Complexity Assuming P ≠ NP
• Minimal NFA Problems are Hard
• Minimizing nfa's and regular expressions
• Monitorability for the Hennessy-Milner logic with recursion
• On runtime enforcement via suppressions
• On the complexity of determinizing monitors
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
• Optimized temporal monitors for SystemcC
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Reactive Systems
• Reasoning about infinite computations
• Reasoning with temporal logic on truncated paths.
• Relationships between nondeterministic and deterministic tape complexities
• Results on the propositional \(\mu\)-calculus
• Rudiments of \(\mu\)-calculus
• Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes
• The tractability frontier for NFA minimization
• Theoretical Aspects of Computing - ICTAC 2004

Cited in

(7)

• On bidirectional runtime enforcement
• Monitorability for the Hennessy-Milner logic with recursion
• Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
• A theory of monitors
• On first-order runtime enforcement of branching-time properties
• Consistently-detecting monitors
• On the complexity of determinizing monitors

Describes a project that uses

Uses Software

• Java-MOP

This page was built for publication: Determinizing monitors for HML with recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2291832)