(Downloads - 0)
For more info about our services contact : help@bestpfe.com
Table of contents
1 Introduction
1.1 Bisimilarity for CCP
1.2 Labeled Semantics
1.3 Algorithms
1.4 From Weak to Strong Bisimilarity
1.5 Summary of Contributions and Organization
1.6 Publications from this Dissertation
2 Deriving Labels and Bisimilarity for CCP
2.1 Background
2.1.1 Constraint Systems
2.1.2 Syntax
2.1.3 Reduction Semantics
2.1.4 Observational Equivalence
2.2 Saturated Bisimilarity for CCP
2.2.1 Saturated Barbed Bisimilarity
2.2.2 Correspondence with Observational Equivalence
2.3 Labeled Semantics
2.4 Strong and Weak Bisimilarity
2.5 Summary of Contributions and Related Work
3 Partition Refinement for Bisimilarity in CCP
3.1 Background
3.1.1 Partition Refinement
3.2 Irredundant Bisimilarity
3.2.1 Reduction Semantics for Non-deterministic CCP
3.2.2 Labeled Semantics for Non-deterministic CCP
3.2.3 Saturated Bisimilarity in a Non-deterministic CCP Fragment
3.2.4 Soundness and Completeness
3.2.5 Syntactic Bisimilarity and Redundancy
3.2.6 Symbolic and Irredundant Bisimilarity
3.3 Partition Refinement for CCP
3.3.1 Termination
3.3.2 Complexity of the Algorithm
3.4 Summary of Contributions and Related Work
4 ReducingWeak to Strong Bisimilarity in CCP
4.1 Background
4.1.1 Reducing Weak to Strong Bisimilarity
4.2 Defining a New Saturation Method for CCP
4.2.1 A New Saturation Method
4.2.2 A Remark about our Saturation in CCS
4.2.3 Soundness and Completeness
4.3 Correspondence between ≈˙ sb, ∼˙ sym, ∼˙ I
4.4 Algorithm for the Weak Notion of the CCP Partition Refinement Algorithm
4.5 Summary of Contributions and Related Work
5 Conclusions
A Implementation and Experiments for the CCP Partition Refinement
A.1 Programming Language
A.2 Abstract Data Types
A.2.1 Implementation Layout
A.2.2 Layout of the Automaton
A.2.3 Layout of the Redundant Class
A.2.4 Layout of a Tool to Verify Bisimilarity in CCP
A.3 Procedures and Functions
A.3.1 Calculating Irredundancy
A.3.2 Strong Prerefinement
A.3.3 Weak Prerefinement
A.3.4 Final Algorithm
A.3.5 Final Strong Algorithm
A.3.6 Saturation
A.3.7 Final Weak Algorithm
A.4 Results and Examples
A.4.1 Transitions/Nodes
A.4.2 Percentage of Same Labels
A.4.3 Percentage of Configurations Satisfying the Same Barb
A.4.4 Percentage of Dominated Transitions
A.4.5 Time vs Branches
A.5 Summary of Contributions and Related Work
