Foundations of Software Science and Computational Structures

Name: Foundations of Software Science and Computational Structures | 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012, Proceedings

Lars Birkedal(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. März 2012

XVII, 484 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-28729-9 (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

Title Page
Foreword
Preface
Organization
Table of Contents
Querying UML Class Diagrams
Introduction
Theoretical Background
UML Class Diagrams
Querying Lean UML Class Diagrams
Formalizing Lean UCDs
Query Answering under Lean UCDs
Discussion and Future Work
References
Bicategories of Concurrent Games (Invited Paper)
Introduction
Event Structures
Maps of Event Structures
Process Operations
Projection
Event Structures with Polarities
Operations
Pre-strategies
Composing Pre-strategies
Concurrent Copy-Cat
Strategies
The Bicategory of Concurrent Games and Strategies
The Subcategory of Deterministic Strategies
From Strategies to Profunctors
Winning Strategies
Operations
The Bicategory of Winning Strategies
Applications
Imperfect Information
Linear Strategies
Conclusion
References
Fibrational Induction Meets Effects
Introduction
Categorical Preliminaries
Effectful Data Types and an Effectful Induction Rule
Induction in a Fibrational Setting
Effectful Induction
A More Logical Treatment of Effectful Induction
Conclusions, Related Work, and Future Work
References
A Coalgebraic Perspective on Minimization and Determinization
Introduction
Background Material on Coalgebras
Minimization via (E,M)-Factorizations
Determinization via Reflections
Conclusion, Related and Future Work
References
When Is a Container a Comonad?
Introduction
Containers
Containers
Interpretation of Containers
Monoidal Structure
Constructions of Containers
Directed Containers
Directed Containers
Interpretation of Directed Containers
Constructions of Directed Containers
Focussing
Containers $$ Comonads = Directed Containers
Containers $$ Monads = ?
Related Work
Conclusions and Future Work
References
Well-Pointed Coalgebras (Extended Abstract)
Introduction
Well-Founded Coalgebras
Well-Pointed Coalgebras
Examples of Well-Pointed Coalgebras
Conclusions
References
Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs
Introduction
First Order Theories of Combinators
Combining Interactive and Automatic Proofs in First Order Logic
First Order Logic in Agda
Combining Agda with Automatic Theorem Provers
Implementing FOTC for PCF in Agda
An Example with Nested Recursion
Adding Inductive and Coinductive Predicates
Inductive Predicates
An Example with Higher-Order Recursion
Coinductive Predicates
A Kahn Network for the Alternating Bit Protocol
Conclusions and Related Work
References
Applicative Bisimulations for Delimited-Control Operators
Introduction
The Language ? S
Syntax
Reduction Semantics
Contextual Equivalence
Bisimilarity for ? S
Labelled Transition System
Applicative Bisimilarity
Soundness
Completeness and Context Lemma
Relation to CPS Equivalence
Axiomatization of Delimited Continuations
Kameyama and Hasegawa's Axioms through Bisimilarity
Bisimilarity and CPS Equivalence
Conclusion
References
Effective Characterizations of Simple Fragments of Temporal Logic Using Prophetic Automata
Introduction
Basic Notation and Background
Reverse Deterministic Büchi Automata
Temporal Logic
From Temporal Logic to CMA's
General Approach and Individual Results
The General Approach
Characterization of the Individual Fragments
Proof Techniques
Characterization of the {XF}-Fragment
Effectiveness and Computational Complexity
Conclusion
References
Improved Ramsey-Based Büchi Complementation
Introduction
Preliminaries
The Ramsey-Based Approach
Reducing State Space
Subset Construction
Merging Transition Profiles
Experimental Results
Preorder-Based Optimization
Conclusion
References
Extending H1-Clauses with Path Disequalities
Introduction
Basics
HornClauses
Automata Classes and Expressiveness
H1-Normalization
Resolution
Splitting
Propagation
Conclusion
References
Brookes Is Relaxed, Almost!
Introduction
Overview of the Paper
Operational Semantics
Denotational Semantics
Full Abstraction
Examples and Laws
Conclusion
References
Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
Introduction
Nondeterministic and Probabilistic Processes
Trace Equivalences for NPLTS Models
Testing Equivalences for NPLTS Models
Trace-by-Trace Redefinition of Testing Equivalence
Placing Trace-by-Trace Testing in the Spectrum
Trace-by-Trace Testing for GPLTS and RPLTS Models
Conclusion
References
Is It a "Good" Encoding of Mixed Choice?
Introduction
Technical Preliminaries
The p- Calculus
Abbreviations
Quality Criteria for Encodings
Encoding Mixed Choice
Distributability
Conclusion
References
Event Structure Semantics of Parallel Extrusion in the Pi-Calculus
Introduction
Free Name Passing
The Causal Links Created by Name Extrusion
The -Calculus
Event Structures
Free Name Passing
Scope Extrusion
Event Structure with Bound Names
Subjective and Objective Causality
The Meaning of Labelled Causality
Disjunctive Causality
Related Work
References
Narcissists Are Easy, Stepmothers Are Hard
Introduction
Coalgebraic Logics with Self-reference
The Depth-1 Fragment in Coalgebraic Semantics
The Depth-2 Fragment in Kripke Semantics
F2(Kn,I) Is PSPACE-Complete
F2(Kn,I,@) Is PSPACE-Complete
F2(Kn,I,@,A) Is EXPTIME-Complete
Embedding the Guarded Fragment
Conclusion
References
On Nominal Regular Languages with Binders
Introduction
Representing Transactions
Languages, Automata and Regular Expressions, with Binders
A Kleene Theorem
Closure Properties
Conclusion
References
Robustness of Structurally Equivalent Concurrent Parity Games
Introduction
Definitions
Markov Chains with Multi-discounted and Parity Objectives
Value Continuity for Parity Objectives
Bounds for Structurally Equivalent Turn-Based Stochastic Parity Games
Value Continuity for Concurrent Parity Games
Conclusion
References
Subgame Perfection for Equilibria in Quantitative Reachability Games
Introduction
Preliminaries
Games, Strategy Profiles and Equilibria
Unraveling
Kuhn's Theorem
Subgame Perfection
Decidability of the Existence of a Secure Equilibrium
Conclusion and Perspectives
References
Concurrent Games with Ordered Objectives
Introduction
Preliminaries
Concurrent Games
Winning Objectives
Nash Equilibria
Decision Problems
Preliminary Lemma
Reachability Objectives
General Case
Simple Cases
Safety Objectives
Büchi Objectives
Reduction to Zero-Sum Games
Applications of the Reduction
Conclusion
References
Full Abstraction for Set-Based Models of the Symmetric Interaction Combinators
Introduction
The Symmetric Interaction Combinators
Nets
Reductions and Equivalences
Denotational Semantics
Interaction Sets
Edifices
Approximations and Full Abstraction
A Fully Abstract Model
References
On Distributability of Petri Nets (Extended Abstract)
Introduction
Basic Notions
Distributed Systems
Distributable Systems
Petri Nets with Reversible Transitions
The Conflict Replicating Implementation
Conclusion
References
Functions as Session-Typed Processes
Introduction
From the -Calculus to the -Calculus
Interpreting the ?-Calculus in the Linear ?- Calculus
From Natural Deduction to Sequent Calculus
Linear Logic and Session Types
Composing the Translations
Soundness and Completeness
Concluding Remarks
References
Deriving Bisimulation Congruences for Conditional Reactive Systems
Introduction
Conditional Reactive Systems
Reactive Systems with Conditions
Representative Squares
Operations on Conditions
Finiteness Assumptions
Label Derivation and Saturated Bisimilarity
Bisimilarity for Conditional Reactive Systems
An Alternative Characterization
Comparison
Conclusion
References
First-Order Model Checking on Nested Pushdown Trees is Complete for Doubly Exponential Alternating Time
Introduction
Related Work
Outline
Preliminaries
Interpretations
Nested Pushdown Trees
The Interpretation Method
Classes of Special Trees
Iterative Definitions and Prescribed Sets
Lower Bounds for Model Checking via Interpretations
Interpretation of Trees in Linear Orders
Reduction of Linear Orders to NPT
Short Formulas for Paths of Exponential Length
Nodes with Many Ancestors
Interpretation of Order and Monadic Quantification
Conclusions
References
Model Checking Languages of Data Words
Introduction
Data Words and Data Multi-pushdown Automata
Monadic Second-Order Logic
Model Checking DMPA
Conclusion
References
Branching-Time Model Checking of Parametric One-Counter Automata
Introduction
Preliminaries
Model Checking POCA
Model Checking EF on POCA
Model Checking ML on POCA
Model Checking SOCA
Model Checking ML on SOCA
Model Checking EF on SOCA
Proof Sketch of Lemma 8
Conclusion
References
Synthesizing Probabilistic Composers
Introduction
Preliminaries
Control-Flow Composition
Defining the Synthesis and Realizability Problems
The Expressive Power of Probabilistic Composers
Embedded Parity Specifications
DPW Specifications
Synthesizing Probabilistic Composers
Discussion
References
On the Complexity of Computing Probabilistic Bisimilarity
Introduction
Probabilistic Bisimilarity
The Bisimilarity Pseudometric
Matchings, Couplings and the Kantorovich Metric
Algorithms for Bisimilarity Pseudometrics
The Discounted Case
The Undiscounted Case
Conclusion
References
Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation
Introduction
Preliminaries
Probabilistic Transition System Specifications
The ntf/ntx Format and the Congruence Theorem
Modular Properties
Tracing Bisimulation
Concluding Remarks
References
On the Complexity of the Equivalence Problem for Probabilistic Automata
Introduction
Preliminaries
Complexity Classes
Sequence Spaces
Weighted Automata
Weighted Cost Automata
Pushdown Automata and Arithmetic Circuits
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken