Invited Talks.- Refinement and Verification Applied to an In-Flight Data Acquisition Unit*.- A Deductive Proof System for CTL*.- Event-State Duality: The Enriched Case.- Expressive Power of Temporal Logics.- Types, or: Where's the Difference Between CCS and ??.- Invited Tutorials.- to Modal and Temporal Mu-Calculi.- Types for Cryptographic Protocols.- Verification, Model Checking.- Network Invariants in Action*.- Regular Model Checking Made Simple and Effcient*.- A Hierarchy of Polynomial-Time Computable Simulations for Automata.- A Decidable Class of Asynchronous Distributed Controllers.- Alphabet-Based Synchronisation is Exponentially Cheaper.- Safe Realizability of High-Level Message Sequence Charts*.- Widening the Boundary between Decidable and Undecidable Hybrid Systems*.- Logic.- A Spatial Logic for Concurrency (Part II).- Reducing Model Checking from Multi-valued CTL* to CTL*.- Local Model Checking Games for Fixed Point Logic with Chop.- A Decidable Fixpoint Logic for Time-Outs*.- Mobility.- A Calculus of Mobile Resources*.- Using Ambients to Control Resources*.- Typing and Subtyping Mobility in Boxed Ambients*.- Orchestrating Transactions in Join Calculus*.- Probabilistic Systems.- Simulation for Continuous-Time Markov Chains.- Weak Bisimulation is Sound and Complete for PCTL*.- Decision Algorithms for Probabilistic Bisimulation*.- Models of Computation, Process Algebra.- Axiomatizing an Algebra of Step Reactions for Synchronous Languages.- Regular Sets of Pomsets with Autoconcurrency.- The Fusion Machine.- HOPLA-A Higher-Order Process Language.- A First Order Coalgebraic Model of ?-Calculus Early Observational Equivalence*.- Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes.- Security.- A Framework for the Analysis of SecurityProtocols*.- On Name Generation and Set-Based Analysis in the Dolev-Yao Model.- On the Decidability of Cryptographic Protocols with Open-Ended Data Structures.- Petri Nets.- Causality Semantics of Petri Nets with Weighted Inhibitor Arcs.- Refinement-Robust Fairness.- Bisimulation.- Decidability of Strong Bisimilarity for Timed BPP.- Undecidability of Weak Bisimilarity for Pushdown Processes.- Why Is Simulation Harder than Bisimulation?.
Inhaltsverzeichnis
Invited Talks. - Refinement and Verification Applied to an In-Flight Data Acquisition Unit*. - A Deductive Proof System for CTL*. - Event-State Duality: The Enriched Case. - Expressive Power of Temporal Logics. - Types, or: Where s the Difference Between CCS and ? ? . - Invited Tutorials. - to Modal and Temporal Mu-Calculi. - Types for Cryptographic Protocols. - Verification, Model Checking. - Network Invariants in Action*. - Regular Model Checking Made Simple and Effcient*. - A Hierarchy of Polynomial-Time Computable Simulations for Automata. - A Decidable Class of Asynchronous Distributed Controllers. - Alphabet-Based Synchronisation is Exponentially Cheaper. - Safe Realizability of High-Level Message Sequence Charts*. - Widening the Boundary between Decidable and Undecidable Hybrid Systems*. - Logic. - A Spatial Logic for Concurrency (Part II). - Reducing Model Checking from Multi-valued CTL* to CTL*. - Local Model Checking Games for Fixed Point Logic with Chop. - A Decidable Fixpoint Logic for Time-Outs*. - Mobility. - A Calculus of Mobile Resources*. - Using Ambients to Control Resources*. - Typing and Subtyping Mobility in Boxed Ambients*. - Orchestrating Transactions in Join Calculus*. - Probabilistic Systems. - Simulation for Continuous-Time Markov Chains. - Weak Bisimulation is Sound and Complete for PCTL*. - Decision Algorithms for Probabilistic Bisimulation*. - Models of Computation, Process Algebra. - Axiomatizing an Algebra of Step Reactions for Synchronous Languages. - Regular Sets of Pomsets with Autoconcurrency. - The Fusion Machine. - HOPLA A Higher-Order Process Language. - A First Order Coalgebraic Model of ? -Calculus Early Observational Equivalence*. - Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes. - Security. - A Framework for the Analysis of SecurityProtocols*. - On Name Generation and Set-Based Analysis in the Dolev-Yao Model. - On the Decidability of Cryptographic Protocols with Open-Ended Data Structures. - Petri Nets. - Causality Semantics of Petri Nets with Weighted Inhibitor Arcs. - Refinement-Robust Fairness. - Bisimulation. - Decidability of Strong Bisimilarity for Timed BPP. - Undecidability of Weak Bisimilarity for Pushdown Processes. - Why Is Simulation Harder than Bisimulation? .
