scientific article; zbMATH DE number 3974280

MaRDI QIDQ3740223zbMATH OpenFDO

Authors Moshe Y. Vardi

Publication date 1985

zbMATH Keywords

infinite computationslooppropositional dynamic logicrepeatstrongest postconditions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Eliminating ``converse from converse PDL
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• PDL with intersection and converse: satisfiability and infinite-state model checking
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• The propositional dynamic logic of deterministic, well-structured programs

Cited in

(10)

• Interactions between knowledge, action and commitment within agent dynamic logic
• Eliminating ``converse from converse PDL
• Answering regular path queries in expressive description logics via alternating tree-automata
• Model checking propositional dynamic logic with all extras
• Nondeterministic program schemata and their relation to dynamic logic
• \textit{Once} and \textit{for all}
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• A minimal logic for interactive epistemology
• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Automated temporal reasoning about reactive systems

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 Q3740223)