On the Power of Labels in Transition Systems | Zendy

Jiřı́ Srba | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

On the Power of Labels in Transition Systems

Author(s) -

Jiřı́ Srba

Publication year - 2001

Publication title -

brics report series

Language(s) - English

Resource type - Journals

eISSN - 1601-5355

pISSN - 0909-0878

DOI - 10.7146/brics.v8i19.21680

Subject(s) - decidability , petri net , reduction (mathematics) , transition system , satisfiability , class (philosophy) , automaton , model checking , discrete mathematics , mathematics , computer science , theoretical computer science , algorithm , artificial intelligence , geometry

In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.

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