Proving correctness of labeled transition systems by semantic tableaux | Zendy

Wolfgang May | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Proving correctness of labeled transition systems by semantic tableaux

Author(s) -

Wolfgang May

Publication year - 1997

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

DOI - 10.1007/bfb0027419

Subject(s) - correctness , computer science , transition system , temporal logic , semantics (computer science) , modal logic , theoretical computer science , model checking , modal , kripke structure , programming language , algorithm , chemistry , polymer chemistry

The paper presents a method for formally proving correctness of processes specified by transition systems which is based on a tableau calculus for an extended temporal logic. The model-theoretic semantics is given by labeled Kripke structures, incorporating information about the actions performed in transitions. Extending first-order CTL for handling action labels, the multi-modal logic MCTL is defined which is well-suited for specifying transition systems and their properties. For MCTL, a tableau semantics and -calulus is presented, allowing formal verification.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research