Reactive Systems and Timed CCP

For more info about our services contact : help@bestpfe.com

Table of contents

1 Introduction 
1.1 Contributions and Organization
1.2 Publications from this Dissertation
2 Preliminaries 
2.1 Process Calculi
2.2 The π-calculus
2.2.1 Names and Actions
2.2.2 Operational Semantics
2.2.3 An Example of Mobility
2.3 Concurrent Constraint Programming
2.3.1 Reactive Systems and Timed CCP
2.4 First-Order Linear-Time Temporal Logic
2.4.1 Semantics of FLTL
3 Syntax and Operational Semantics 
3.1 Constraint Systems
3.2 Timed CCP (tcc)
3.3 Abstractions and Universal Timed CCP
3.3.1 Recursion in utcc
3.4 Structural Operational Semantics
3.5 Properties of the Internal Transitions
3.6 Mobility in utcc
3.7 Input-Output Behavior
3.8 Infinite Internal Behavior
3.9 Summary and Related Work
4 Symbolic Semantics 
4.1 Symbolic Intuitions
4.1.1 Future-Free Temporal Formulae as Constraints
4.2 Symbolic Reductions
4.2.1 The Abstracted-Unless Free Fragment
4.2.2 Past-Monotonic Sequences
4.3 Properties of the Symbolic Semantics
4.3.1 Normal Form of Processes
4.3.2 Symbolic Output Invariance
4.3.3 The Monotonic Fragment
4.4 Relating the SOS and the Symbolic Semantics
4.4.1 Elimination of local processes
4.4.2 Local-Free Fragment
4.4.3 Semantic Correspondence
4.5 Summary and Related Work
5 Temporal Logic Characterization of utcc Processes 
5.1 utcc processes as FLTL formulae
5.2 FLTL Correspondence
5.2.1 Symbolic Reductions Correspond to FLTL Deductions
5.2.2 Deductions in FLTL correspond to Symbolic Reductions
5.3 Summary and Related Work
6 Expressiveness of utcc and Undecidability of FLTL ذ
6.1 Minsky Machines
6.2 Encoding Minsky Machines into utcc
6.2.1 Representation of Numbers in utcc
6.2.2 Encoding of Machine Configurations
6.3 Correctness of the Encoding
6.3.1 Derivations in the Minsky Machine and utcc Observables
6.3.2 Termination and Computations of the Minsky Machine
6.4 Undecidability of monadic FLTL
6.5 Encoding the λ-calculus into utcc
6.5.1 The call-by-name λ-calculus
6.5.2 Encoding the λ-calculus into the π-calculus
6.5.3 Encoding the λ-calculus into utcc
6.5.4 Correctness of the Encoding
6.6 Summary and Related Work
7 Denotational Semantics 
7.1 Symbolic Behavior as Closure Operators
7.1.1 Symbolic Input-Output Relation
7.1.2 Retrieving the Input-Output Behavior
7.2 Denotational Semantics for utcc
7.2.1 Semantic Equation for Abstractions Using ~x-variants
7.3 Full Abstraction
7.3.1 Soundness of the Denotation
7.3.2 Completeness of the Denotation
7.4 Summary and Related Work
8 Closure Operators for Security 
8.1 The modeling language: SCCP
8.1.1 Processes in SCCP
8.2 Dolev-Yao Constraint System
8.3 Modeling a Security Protocol in SCCP
8.4 Closure Operator semantics for SCCP
8.4.1 Closure Properties of SCCP
8.5 Verification of Secrecy Properties
8.6 Reachability Analysis in SCCP
8.7 Summary and Related Work
9 Applications 
9.1 Service Oriented Computing
9.2 A Language for Structured Communication
9.2.1 Operational Semantics of HVK
9.2.2 An Example
9.3 A Declarative Interpretation for Sessions
9.3.1 Operational Correspondence
9.4 HVK-T: An Temporal extension of HVK
9.4.1 Case Study: Electronic booking
9.4.2 Exploiting the Logic Correspondence
9.5 Multimedia Interaction Systems
9.6 Dynamic Interactive Scores
9.6.1 A utcc model for Dynamic Interactive Scores
9.6.2 Verification of the Model
9.7 A Model for Music Improvisation
9.8 Summary and Related Work
10 Abstract Semantics and Static Analysis of utcc Programs 
10.1 Static Analysis and Abstract Interpretation
10.1.1 Static Analysis of Timed CCP Programs
10.2 Constraint Systems as Information Systems
10.2.1 Recursion and Parameter Passing
10.3 A Denotational model for tcc and utcc
10.3.1 Semantic Correspondence
10.4 Abstract Interpretation Framework
10.4.1 Abstract Constraint Systems
10.4.2 Abstract Semantics
10.4.3 Soundness of the Approximation
10.5 Applications
10.5.1 Groundness Analysis
10.5.2 Analysis of Reactive Systems
10.5.3 Analyzing Secrecy Properties
10.5.4 A prototypical implementation
10.6 Summary and Related Work
11 Concluding Remarks 149
11.1 Overview
11.2 Future Directions
Bibliography 
A Incompleteness of Monadic FLTL: Alternative Proof
A.1 Encoding Minsky Machines
A.2 Encoding of Numbers and Configurations
A.3 Monadic FLTL is Undecidable
Index