scientific article; zbMATH DE number 176729

zbMATH Open0769.68024MaRDI QIDQ4036558FDOQ4036558

Authors Rance Cleaveland, Bernhard Steffen 

Publication date 18 May 1993

zbMATH Keywords

fixed point logicmodel-checking algorithmcomputing preordersefficient computation of behavioral relations between processesfragment of the modal mu-calculus

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Modal logic (including the logic of norms) (03B45) Other applications of logic (03B80)

Recommendations

• Mechanizing logical relations
• scientific article; zbMATH DE number 3852428
• Behavioral algebraization of logics
• A logic of behaviour in context
• Behavioral program logic
• Computational logic
• Reasoning, Logic and Computation
• Computation on structures. Behavioural theory, logic, complexity
• Computational logic and the social
• Logical behaviors

Cited in

(14)

• Complete proof systems for weighted modal logic
• Verification and comparison of transition systems
• When are prime formulae characteristic?
• A linear-time model-checking algorithm for the alternation-free modal mu-calculus
• Local model checking for context-free processes
• scientific article; zbMATH DE number 4014516 (Why is no real title available?)
• When are prime formulae characteristic?
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• CEGAR for compositional analysis of qualitative properties in Markov decision processes
• Generating diagnostic information for behavioral preorders
• The expressive power of implicit specifications
• Characteristic formulae for timed autoamta
• Data flow analysis as model checking
• Model-checking process equivalences

This page was built for publication:

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