A logic for the description of non-deterministic programs and their properties

DOI10.1016/S0019-9958(86)80038-9zbMath0591.68017MaRDI QIDQ3719799

Joseph Sifakis, Susanne Graf

Publication date: 1986

Published in: Information and Control (Search for Journal in Brave)

zbMATH Keywords

verificationrecursionmodal logicscomplete deductive systemspecification and proof of programsSynchronization Tree Logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

A logic for the specification and proof of regular controllable processes of CCS ⋮ Extension of synthesis algorithm of recursive processes to \(\mu\)-calculus ⋮ Conjunction on processes: Full abstraction via ready-tree semantics ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\) ⋮ Proof systems for satisfiability in Hennessy-Milner logic with recursion ⋮ On hierarchically developing reactive systems ⋮ Compositionality and bisimulation: A negative result ⋮ Graphical versus logical specifications ⋮ Parametric and Quantitative Extensions of Modal Transition Systems ⋮ Modal logics for communicating systems ⋮ Ready simulation for concurrency: it's logical! ⋮ Connection between logical and algebraic approaches to concurrent systems ⋮ Encoding safety in \(\mathrm{CLL}_R\) ⋮ A Logical Process Calculus ⋮ Inductive synthesis of recursive processes from logical properties

This page was built for publication: A logic for the description of non-deterministic programs and their properties