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

DOI10.1016/S0019-9958(86)80038-9MaRDI QIDQ3719799zbMATH OpenFDO

Authors Susanne Graf, Joseph Sifakis

Publication date 1986

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

Full work available at URL https://doi.org/10.1016/S0019-9958(86)80038-9

zbMATH Keywords

complete deductive systemmodal logicsrecursionspecification and proof of programsSynchronization Tree Logicverification

Mathematics Subject Classification ID

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

Recommendations

• Logical analysis of demonic nondeterministic programs
• scientific article; zbMATH DE number 4200180
• scientific article; zbMATH DE number 1303442
• A nondeterministic program logic
• Partiality and nondeterminacy in program proofs

Cited in

(23)

• A logic for the specification and proof of regular controllable processes of CCS
• While-programs with nondeterministic assignments and the logic ALNA
• Compositionality and bisimulation: A negative result
• Extension of synthesis algorithm of recursive processes to -calculus
• Inductive synthesis of recursive processes from logical properties
• On hierarchically developing reactive systems
• Encoding safety in \(\mathrm{CLL}_R\)
• Characteristic invariants in Hennessy-Milner logic
• A logical process calculus
• Connection between logical and algebraic approaches to concurrent systems
• scientific article; zbMATH DE number 3913664 (Why is no real title available?)
• scientific article; zbMATH DE number 139633 (Why is no real title available?)
• scientific article; zbMATH DE number 4123706 (Why is no real title available?)
• scientific article; zbMATH DE number 1354147 (Why is no real title available?)
• Parametric and quantitative extensions of modal transition systems
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Modal logics for communicating systems
• Logical analysis of demonic nondeterministic programs
• Graphical versus logical specifications
• Conjunction on processes: Full abstraction via ready-tree semantics
• Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\)
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Ready simulation for concurrency: it's logical!

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

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