A tableau proof system for a mazurkiewicz trace logic with fixpoints

DOI10.1007/BFb0027421zbMath1412.68246OpenAlexW1562348633MaRDI QIDQ4610334

Peter Niebert, Barbara Sprick

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0027421

zbMATH Keywords

model checkingtemporal logicproof systematomic proposition

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• An automata theoretic decision procedure for the propositional mu- calculus
• A partial approach to model checking
• Automata for the modal μ-calculus and related results
• A ν-calculus with local views for systems of sequential agents
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Action refinement and property inheritance in systems of sequential agents

This page was built for publication: A tableau proof system for a mazurkiewicz trace logic with fixpoints