scientific article

zbMath0647.68012MaRDI QIDQ3792217

Kim Guldstrand Larsen

Publication date: 1988

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

livenesssafetyproof systemsPrologdecision procedureHennessy-Milner logic with recursionmaximal interpretationsverifyingMinimal interpretations of formulas

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 (27)

Model checking and boolean graphs ⋮ A modal logic for message passing processes ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Duality for modal \(\mu\)-logics ⋮ Data flow analysis as model checking ⋮ Petri nets, traces, and local model checking ⋮ Action refinement and property inheritance in systems of sequential agents ⋮ A functional programming approach to the specification and verification of concurrent systems ⋮ A refinement calculus for specifications in Hennessy-Milner logic with recursion ⋮ Proof systems for satisfiability in Hennessy-Milner logic with recursion ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ Bisimulation through probabilistic testing ⋮ A note on model checking the modal \(\nu\)-calculus ⋮ Compositional checking of satisfaction ⋮ The expressive power of implicit specifications ⋮ Compositional checking of satisfaction ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Complete proof systems for weighted modal logic ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ An action based framework for verifying logical and behavioural properties of concurrent systems ⋮ A linear-time model-checking algorithm for the alternation-free modal mu-calculus ⋮ A linear-time model-checking algorithm for the alternation-free modal mu- calculus ⋮ Petri nets, traces, and local model checking ⋮ A compositional \(\mu\)-calculus proof system for statecharts processes ⋮ Swinging types=functions+relations+transition systems ⋮ A complete modal proof system for HAL: the Herbrand agent language ⋮ Compositional verification of asynchronous concurrent systems using CADP

This page was built for publication: