Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

14 years 2 months ago

Download www.win.tue.nl

Abstract. In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness and illustrate the approach with two examples. We also provide small adaptations to obtain similar transformations for strong and weak bisimulations and simulation equivalences.

Taolue Chen, Bas Ploeger, Jaco van de Pol, Tim A.

Real-time Traffic

Branching Bisimulation Problem | CONCUR 2007 | Distributed And Parallel Computing | Linear Process Format | Parameterized Boolean Equation |

claim paper

» Solving Alternating Boolean Equation Systems in Answer Set Programming

» Infinite Families of Finite String Rewriting Systems and Their Confluence

» Model Checking Synchronized Products of Infinite Transition Systems

» Static Analysis using Parameterised Boolean Equation Systems

» Dependent types and program equivalence

» Computing the Algebraic Immunity Efficiently

» OntheFly Reachability and Cycle Detection for Recursive State Machines

» Predicate Diagrams for the Verification of RealTime Systems

Post Info
More Details (n/a)

Added	14 Aug 2010
Updated	14 Aug 2010
Type	Conference
Year	2007
Where	CONCUR
Authors	Taolue Chen, Bas Ploeger, Jaco van de Pol, Tim A. C. Willemse

Comments (0)

Sciweavers

Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

Branching Bisimulation Problem | CONCUR 2007 | Distributed And Parallel Computing | Linear Process Format | Parameterized Boolean Equation |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers