Propositional Dynamic Logic (PDL) [1] is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking. PDL is what is known as a modal … full description “A Cyclic Prover for Propositional Dynamic Logic (available)”
Category: Logic
Bisimulation Algorithmics (available)
Labelled transition systems are a crucial abstraction to understandcomplex and distributed systems. Bisimulation, in its many variations,is conceptually at the core of many verification tools. One such toolis OvenMPST. OvenMPST is a tool for validatingand handling multiparty protocol specifications. In this tool,bisimulation plays a central role in establishing that a protocol iswell formed and correctly … full description “Bisimulation Algorithmics (available)”