CONCUR 2011 -- Concurrency Theory

Name: CONCUR 2011 -- Concurrency Theory | 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011, Proceedings

Joost-Pieter Katoen Barbara König(Herausgeber*in)

Springer (Verlag)

Erschienen am 27. August 2011

XIV, 560 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-23217-6 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Title
Preface
Organization
Table of Contents
Invited Talks
Carrying Probabilities to the Infinite World
Introduction
Transition Systems
Petri Nets
Model
Safety Properties
Algorithm
Finite Span
VASS
Markov Chains
Decisive Markov Chains
Sufficient Condition I
Sufficient Condition II
Probabilistic Petri Nets
Communicating Processes
Qualitative Analysis
Reachability
Repeated Reachability
Quantitative Analysis
References
Generalized Universality
Introduction
State Machine Replication: The Classics
Model
Protocol
Correctness
Generalized State Machine Replication
Properties
K-set Consensus
From 1 to k
Vectors of Adopt-Commit Objects
Protocol
Correctness
Concluding Remarks
References
Causal Nets: A Modeling Language Tailored towards Process Discovery
Motivation
Causal Nets
Definition
Valid Sequences
Soundness
Relating C-nets and Petri Nets
Petri Nets and WF-nets
Mapping WF-nets onto C-nets
Mapping C-nets onto WF-nets
Application of C-nets in ProM
Model Management and Conversion
Model-Based Verification
Process Discovery
Conformance Checking and Performance Analysis
Conclusion
References
On Causal Semantics of Petri Nets (Extended Abstract)
Introduction
Place Transition Systems
Processes of Place/Transition Systems
Conflicts in Place/Transition Systems
A Conflict-Free Net Has Exactly One Maximal Run
BD-Processes Fit Structural Conflict Nets
References
Real-Time Systems
On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing
Introduction
Timed Temporal Logics: Syntax and Semantics
Preliminaries
Metric Temporal Logics
Freeze Logics
EF Games for IvMTL[UI,SI]
Separating Sub Logics of MTL[UI,SI]
TPTL and MTL
Comparing TTL[X,Y] with MTL[UI,SI] Fragments
Embedding TTL[X, Y] into MITL[FI,PI]:
On Limited Expressive Power of TTL[X, Y]
References
Timed Automata Can Always Be Made Implementable
Introduction
Timed Models and Specifications
Timed Transition Systems and Behavioural Relations
Timed Automata
Quantitative Extension of Computation Tree Logic
Implementability
Robustness
Samplability
Main Result of the Paper
Making Timed Automata Robust and Samplable
Proof of Correctness
Properties of Regions
Proof of Robustness
Proof of Samplability
Proof of Safety Preservation (Ready Simulation)
Conclusion
References
Coarse Abstractions Make Zeno Behaviours Difficult to Detect
Introduction
Zeno-Related Problems for Timed Automata
Timed Automata
Symbolic Semantics, Zenoness and Non-zenoness Problems
Non-zenoness is NP-complete for ExtraLU
Finding Non-zeno Runs
Reduced Guessing Zone Graph rGZGa(A)
Polynomial Algorithms for NZPa
The Zenoness Problem
Reducing 3SAT to ZPa with Abstraction ExtraLU
Finding Zeno Paths
Weakening the U Bounds
Conclusion
References
Probabilistic Systems
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
Introduction
Preliminaries
Probabilistic Automaton, PCTL* and Bisimulations
PCTL* and Its Sublogics
Strong Probabilistic Bisimulation
A Novel Strong Bisimulation
Strong 1-depth Bisimulation
Strong Branching Bisimulation
Strong Bisimulation
Taxonomy for Strong Bisimulations
Weak Bisimulations
Branching Probabilistic Bisimulation by Segala
A Novel Weak Branching Bisimulation
Weak Bisimulation
Taxonomy for Weak Bisimulations
Related Work
Conclusion and Future Work
References
A Spectrum of Behavioral Relations over LTSs on Probability Distributions
Introduction
Probabilistic Simulation and Bisimulation
An Operational View of Probabilistic HML
LTS on Distributions
Comparing L and L
States as Abstract Interpretation of Distributions
A Spectrum of Probabilistic Relations over DLTSs
Probabilistic Simulation
Failure Simulation
Related and Future work
References
Fixed-Delay Events in Generalized Semi-Markov Processes Revisited
Introduction
Preliminaries
Generalized Semi-Markov Processes
FrequencyMeasures
Region Graph
Two Fixed-Delay Events
Single-Ticking GSMP
Reaching a BSCC
Frequency in a BSCC
Approximations
Conclusions, Future Work
References
Semantic Analysis of Gossip Protocols for Wireless Sensor Networks
Introduction
A Probabilistic Timed Process Calculus
Probabilistic Labelled Transition Semantics
Time Properties
Simulation Up to Probability
Gossipping without Collisions
Gossipping with Collisions
Conclusions, Future and Related Work
References
Automata
An Automaton over Data Words That Captures EMSO Logic
Introduction
DataWords
Logic
Class Register Automata
Realizability of EMSO Specifications
From Automata to Logic
Conclusion
References
Advanced Ramsey-Based B¨uchi Automata Inclusion Testing
Introduction
Preliminaries
Ramsey-Based Language Inclusion Testing
Optimized Language Inclusion Testing
Optimization 1: Minimization of Supergraphs
Optimization 2: Discarding Subsumed Supergraphs
Using Forward Simulation Between A and B
Metagraphs and a New RDGT
The Main Algorithm
Experimental Results
Conclusions
References
Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
Introduction
Multistack Pushdown Systems
Reachability within a Fixed Number of Contexts and Phases
Location Reachability for SMpds
Configuration Reachability for SMpds
Conclusion and Future Work
References
Separation Logic
Granularity and Concurrent Separation Logic
Introduction
Syntax
Petri-Net Semantics
Net Contexts and Substitution
Concurrent Separation Logic
Interference and Ownership Nets
Soundness
Separation
Strength of Race-Freedom
Footprints and Refinement
Conclusions and Related Work
References
Tractable Reasoning in a Fragment of Separation Logic
Introduction
Preliminaries
A Normal Form of SL-Graphs
Computing Entailment via Homomorphisms between SL-Graphs in Normal Form
Syntactic Extensions Leading to Intractability
Conclusion
References
On Locality and the Exchange Law for Concurrent Processes
Introduction
Two Models
Exchange
Algebra
Program Logic
Locality
Local Elements
Lubs and Fixed-points
On Assertions, Triples and Programs
Connections in the Resource Model
Recursion Rule
Conclusion
References
p-Calculus
Typed ?-calculi
Introduction
-calculi
Syntax
Labelled Semantics
A Simple Type System for
Types and Type Environments
Type Judgements and Type Rules
Properties of the Simple Type System
Standard Lemmas
The Subject Reduction Property
Safety in the Simple Type System
Instances of the Simple Type System
The Calculus of Explicit Fusions
The Distributed -calculus
A Type System for Secrecy
Correspondence Types for Authenticity
Conclusions and Further Work
References
Full Abstraction in a Subtyped pi-Calculus with Linear Types
Introduction
A Concise, Subtyped -Calculus
Embedding Functional Subtyping
Embedding Communication Subtyping
Related Work and Further Topics
References
Controlling Reversibility in Higher-Order Pi
Introduction
Informal Presentation
The roll- Calculus and Its High-Level Semantics
Syntax
Operational Semantics
Soundness and Completeness of Backward Reduction in roll-
A Distributed Semantics for roll-
Related Work and Conclusion
References
Petri Nets
A Connector Algebra for P/T Nets Interactions
Introduction
Background
The Tile Model
Nets with Boundaries
Petri Calculus
P/T Nets with Boundaries
Petri Tile Calculus
P/T Nets as Tiles
Petri Tile Calculus as P/T Nets with Boundaries
Related Work
Conclusions
References
Vector Addition System Reversible Reachability Problem
Introduction
Projected Vectors
Vector Addition Systems
Subreachability Graphs
Outline
Displacement Vectors
Reversible Witness Graphs
Extractors
Pumpable Configurations
Deciding The Reversibility Problem
Application : Reversibility Domains
Conclusion
References
Efficient Contextual Unfolding
Introduction
Basic Notions
Encodings of Contextual Nets
Contextual Unfoldings and Their Prefixes
Constructing Finite Prefixes
Two Approaches to Possible Extensions and Concurrency
Computing Possible Extensions
Updating the Concurrency Relation
Discussion: Lazy vs. Eager Approach
Efficient Prefix Construction
Experiments
Conclusions
References
Parameterized Complexity Results for 1-safe Petri Nets
Introduction
Preliminaries
Petri Nets
Logics
Parameters
Lower Bounds for 1-safe Petri Nets and Pebbling
1-safe Petri Nets, Treewidth and Pathwidth
Graph Pebbling Problems, Treewidth and Pathwidth
1-safe Petri Nets and Benefit Depth
Vertex Cover and Model Checking 1-safe Petri Nets
Conclusion
References
Process Algebra and Modeling
The Decidability of the Reachability Problem for CCS!
Introduction
Preliminaries
The Calculus
The Petri Nets
Reachability Problem
Main Idea
Informal Description
Formal Definitions
The Construction of Petri Nets
Base Step
Induction Step
Final Step
Deciding Reachability Problem
Concluding Remark
References
Static Livelock Analysis in CSP
Introduction
CSP: Syntax and Conventions
Operational and Denotational Semantics
Static Livelock Analysis
Structurally Finite-State Processes
Implementation and Experimental Results
Future Work
References
Dynamic Reactive Modules
Introduction
High-Level Description of Dynamic Reactive Modules
Dynamic Discrete Systems
Definitions
Properties
Formal Dynamic Reactive Modules
Conclusions and Future Work
References
Verification
Weak Kripke Structures and LTL
Introduction
Computation Paths and Kripke Structures
Linear-Time Temporal Logic - LTL
LTL Model Checking Problems in NC
coNP-Complete LTL Model Checking Problems
PSPACE-Complete LTL Model Checking Problems
Conclusions
References
EÆcient CTL Model-Checking for Pushdown Systems
Introduction
Preliminaries
The Temporal Logic CTL
PushDown Systems
Alternating Büchi PushDown Systems
Computing the Language of an ABPDS
Characterizing L(BP)
Computing L(BP)
CTL Model-Checking for PushDown Systems
CTL Model-Checking for PushDown Systems with Regular Valuations
Experiments
Related Work
References
Reasoning about Threads with Bounded Lock Chains
Introduction
System Model
Pairwise CFL-Reachability
Lock Causality Automata
Computing LCAs for Operators
The Model Checking Procedure for L(X, F, F)
Conclusion
References
Games
A Temporal Logic for the Interactionof Strategies
Introduction
System Models and BSIL
Turn-Based Game Graphs
BSIL Syntax
BSIL Semantics
Expressiveness of BSIL
Some Properties of BSIL Model Checking Problem
BSIL Model-Checking Algorithm
Computing Path Obligations Passed Down Computation Tree
Procedures for Checking BSIL Properties
Correctness Proof of the Algorithm
Complexities of the Algorithm
Strategy Interaction Logic
Conclusion
References
The Complexity of Nash Equilibria in Limit-Average Games
Introduction
Concurrent Games
Nash Equilibria
Positional Strategies
Stationary Strategies
Pure Strategies
Randomised Strategies
Conclusion
References
Two Variable vs. Linear Temporal Logic in Model Checking and Games
Introduction
Logics and Models
Translating UTL and FO2 to Automata
rom FO2 to Deterministic Parity Automata
From UTL to BLuchi Automata
Verifying Non-Deterministic Systems
Verifying Probabilistic Systems
References
A Compositional Framework for Controller Synthesis
Introduction
Decision Functions, Strategies and Controllers
Compositionality
Game-Based Controller Synthesis
Conclusion
References
Bisimulation
Decidability of Branching Bisimulation on Normed Commutative Context-Free Processes
Introduction
Preliminaries
Decidability via Small Response Property
Normal Form by Squeezing
Small Normal Form
Proof of the Small Response Property
References
Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
Introduction
Preliminaries
The Models
Mayr's PRS Hierarchy
(Regular) Ground Tree Rewrite Systems and Prefix-Recognizable Systems
Containment Results
PADGTRS
Further Containment Results
Separation Results
PAGTRS
GTRSPAD
PDSPAN and PNGTRS
Applications
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken