Proof systems for satisfiability in Hennessy-Milner logic with recursion

DOI10.1016/0304-3975(90)90038-JzbMath0698.68014WikidataQ128111591 ScholiaQ128111591MaRDI QIDQ912592

Kim Guldstrand Larsen

Publication date: 1990

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

livenesssafetyproof systemsdecision procedureprologHennessy-Milner logic with recursionmaximal interpretationsminimal interpretation of formulasverifying

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (37)

Model checking for action-based logics ⋮ Characteristic formulae for fixed-point semantics: a general framework ⋮ Modal logic and the approximation induction principle ⋮ Bidirectional Runtime Enforcement of First-Order Branching-Time Properties ⋮ Model Checking Value-Passing Modal Specifications ⋮ On the complexity of determinizing monitors ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Unnamed Item ⋮ On first-order runtime enforcement of branching-time properties ⋮ The power of reachability testing for timed automata ⋮ Logical characterisations, rule formats and compositionality for input-output conformance simulation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mathematical modal logic: A view of its evolution ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Local model checking for context-free processes ⋮ Local model checking in the modal mu-calculus ⋮ Compositionality and bisimulation: A negative result ⋮ Duality and the completeness of the modal \(\mu\)-calculus ⋮ Local model checking for infinite state spaces ⋮ The complexity of identifying characteristic formulae ⋮ Observing localities ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Introduction to the special issue on runtime verification ⋮ On decidability of recursive weighted logics ⋮ Compositionality for quantitative specifications ⋮ A linear-time-branching-time spectrum for behavioral specification theories ⋮ Determinizing monitors for HML with recursion ⋮ Logical vs. behavioural specifications ⋮ Encoding safety in \(\mathrm{CLL}_R\) ⋮ Full abstractness for a functional/concurrent language with higher-order value-passing ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic ⋮ A complete modal proof system for HAL: the Herbrand agent language ⋮ Monitoring for Silent Actions ⋮ On bidirectional runtime enforcement

Cites Work

• Modal logics for communicating systems
• The temporal logic of branching time
• A logical characterization of observation equivalence
• Calculi for synchrony and asynchrony
• A proof-theoretic characterization of observational equivalence
• A logic for the specification and proof of regular controllable processes of CCS
• A calculus of communicating systems
• A structural approach to operational semantics
• A lattice-theoretical fixpoint theorem and its applications
• A logic for the description of non-deterministic programs and their properties
• Algebraic laws for nondeterminism and concurrency
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof systems for satisfiability in Hennessy-Milner logic with recursion