Theoretical Aspects of Computing - ICTAC 2015

Name: Theoretical Aspects of Computing - ICTAC 2015 | 12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

12th International Colloquium, Cali, Colombia, October 29-31, 2015, Proceedings

Martin Leucker Camilo Rueda Frank D. Valencia(Herausgeber*in)

Springer (Verlag)

Erschienen am 8. Oktober 2015

XXIV, 620 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-25150-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

Intro
Preface
Organization
Invited Talks Abstracts
Contents
Invited Talks
An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem
1 Introduction
2 Definition of Regions
2.1 Definition of a Region: Interior, Exterior, and Border
2.2 Decomposing the Border of a Region
3 Relations Between Regions
3.1 External Regions
3.2 Internal Regions
3.3 Externally Tangent Regions
3.4 Internally Tangent Regions
3.5 Maximal Regions
4 Systems of Connected Regions and Definition of Faces
5 Graphs and Planar Graphs
5.1 Definitions of a Graph and of Graph Vertices
5.2 A Relation Between Vertices
5.3 Definition of Edges
5.4 Graphs with Loops
5.5 Simple Graphs
5.6 Chains in a Graph
5.7 Connected Graphs
5.8 Subgraphs
5.9 Graph Drawings
5.10 More on the Equivalence Relation Between Graph Drawings
5.11 Graph Extension
5.12 Chain Intersections in a Graph
5.13 Planar Graph
5.14 Example of a Non-planar Graph: The Graph K5
5.15 Example of a Non-planar Graph: The Graph K3,3
6 Chain Intersection Axioms
7 The Kuratowski Theorem
8 Conclusion
References
Location Privacy via Geo-Indistinguishability
1 Introduction
1.1 Related Work
1.2 Plan of the Paper
2 Geo-Indistinguishability
2.1 Location Guard
3 Making Geo-Indistinguishability Flexible Over Time and Space.
3.1 Repeated Use Over Time
3.2 Highly Recurrent Locations
3.3 Flexible Behavior Over Space
3.4 A Tiled Mechanism
4 Future Work
References
A Note on Monitors and Büchi Automata
1 Preliminaries
2 Topological Properties
3 Constructions of Monitors
3.1 Monitors for -regular Languages in GF
3.2 General Constructions
4 Monitorable Deterministic Languages
5 Deciding Liveness and Monitorability
5.1 Decidability for Büchi Automata
5.2 Decidability for LTL
5.3 Encoding EXPSPACE Computations
5.4 Proof of Proposition6
6 Conclusion and Outlook
References
Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture)
References
The Proof Technique of Unique Solutions of Contractions
References
On Probabilistic Distributed Strategies
1 Introduction
2 Event Structures [3]
3 Distributed Games and Strategies---the Definitions [4]
4 Probabilistic Event Structures [12]
5 Probabilistic Strategies [15]
5.1 A Bicategory of Probabilistic Strategies
5.2 Extensions: Payoff and Imperfect Information
6 Constructions on Probabilistic Strategies [19]
7 A Limitation
8 A Solution
References
Algebra and Category Theory
Newton Series, Coinductively
1 Introduction
2 Preliminaries: Stream Calculus
3 Four Product Operators
4 Newton Transform
5 Calculating Newton Coefficients
6 Newton Series
7 Weighted Languages
8 Four Rings of Weighted Languages
9 Newton Transform for Languages
10 Newton Series for Languages
11 Discussion
References
Quotienting the Delay Monad by Weak Bisimilarity
1 Introduction
2 The Type Theory Under Consideration
3 Delay Monad
4 Inductive-Like Quotients
5 Multiplication: What Goes Wrong?
6 Axiom of Countable Choice and Streams of Quotients
7 Multiplication: A Solution Using AC
7.1 Delayed Computations as Streams
7.2 Construction of
8 A Monad or an Arrow?
9 Conclusions
References
Inverse Monoids of Higher-Dimensional Strings
1 Introduction
2 Preliminaries
3 Unambiguous Graphs and Connecting Morphisms
4 The Inverse Monoid of Birooted Graphs
5 Languages of Birooted Graphs
6 The Inverse Monoid of Acyclic Birooted Graphs
7 Conclusion
References
A Functorial Bridge Between the Infinitary Affine Lambda-Calculus and Linear Logic
1 Introduction
2 The Infinitary Affine Lambda-Calculus
3 Denotational Semantics
4 Computing Symmetric Monoidal Kan Extensions
5 From Infinitary Affine Terms to Linear Logic
6 Discussion
References
Automata and Formal Languages
Learning Register Automata with Fresh Value Generation
1 Introduction
2 Register Automata
3 Active Automata Learning
4 A Theory of Mappers
5 The Determinizer
6 The Lookahead Oracle
7 The Abstractor
7.1 Mapper Definition
7.2 Counterexample Analysis
8 Evaluation and Comparison
9 Conclusions and Future Work
References
Modeling Product Lines with Kripke Structures and Modal Logic
1 Introduction
2 Feature Models and Partial Product Lines
2.1 Basics of Feature Modeling
2.2 Partial Product Lines: Products as Processes
2.3 Partial Product Lines: From Lattices to Transition Systems
3 Feature Models and Partial Product Lines: Formally
3.1 Feature Models
3.2 Full and Partial Products
3.3 Ppls as Transition Systems
4 Partial Product Kripke Structures and Their Logic
4.1 Partial Product Kripke Structures
4.2 Partial Product Computation Tree Logic
4.3 ppCTL-theory of Feature Models
5 Possible Practical Applications
6 Feature Vs. Event-based Concurrency Modeling
7 Related Work
8 Conclusion
References
Deterministic Regular Expressions with Interleaving
1 Introduction
2 Preliminaries
2.1 Regular Expressions with Interleaving
2.2 Deterministic Regular Expressions with Interleaving
2.3 Computing follow- Sets
3 Weak Determinism of RE(&)
3.1 The First Algorithm
3.2 The Improved Algorithm
4 Strong Determinism of RE(&)
5 Implementations and Experiments
5.1 Weak Determinism
5.2 Weakly Star Normal Form and Strong Determinism
6 Conclusion
References
Concurrency
Rigid Families for CCS and the pi-calculus
1 Introduction
2 A Category of Rigid Families
3 Rigid Families for CCS
3.1 Definitions
3.2 Operational Correspondence with CCS
3.3 Causality and Concurrency in CCS
4 Rigid Families for the pi-calculus
4.1 Labels for the pi-calculus
4.2 Synchronizations
4.3 Operational Correspondence with the pi-calculus
4.4 Causality and Concurrency in the pi-calculus
5 Advanced Criteria
5.1 Realisability
5.2 Structural Congruence
5.3 Reversibility and Stability
6 Conclusions
References
Quotients of Unbounded Parallelism
1 Introduction
2 Shuffles and Quotients
2.1 Operators for Constructing Languages
2.2 Language Quotients
2.3 Rules for Quotients
2.4 Orders and Transition Systems
2.5 Semilinear Sets
2.6 Petri Nets
3 Observations and Results
3.1 Simulating Petri Nets
3.2 Quotients Representable as Finite Trees
3.3 Any Quotient as a Petri Net
4 Related Work
5 Conclusion and Outlook
References
Higher-Order Dynamics in Event Structures
1 Introduction
2 Technical Preliminaries
2.1 Event Structures for Resolvable Conflicts
2.2 Dynamic Causality
3 Generalisation
3.1 Higher Order Dynamics
4 From Configuration Structures to HDES
5 Conclusion
References
Asynchronous Announcements in a Public Channel
1 Introduction
2 Background: Public Announcement Logic
3 Language and Models
3.1 Language
3.2 Models
4 Semantics: The Circularity Problem
4.1 Intuitions
4.2 Circularity
4.3 When the Initial Model Is a Finite Tree
4.4 Announcing Existential Formulas
5 Validities
6 Model Checking
6.1 Propositional Announcements
6.2 Finite Tree Initial Model
6.3 Existential Announcements
7 Related Work
8 Future Work
References
A Totally Distributed Fair Scheduler for Population Protocols by Randomized Handshakes
1 Introduction
2 Population Protocols
3 Related Works : Existing Schedulers
4 The Distributed Probabilistic Fair Handshake Scheduler for Population Protocols
4.1 The Randomized Rendezvous Algorithm
4.2 The Randomized Handshake Scheduler for Population Protocols
4.3 The Fairness of the Handshake Scheduler
5 The Time Complexity of Iterated Population Protocols
5.1 The Iterated Population Protocols
5.2 A General Upper Bound
5.3 Upper Bound When the Interaction Graph Is with Bounded Degree
5.4 Upper Bound When the Interaction Graph Is a Random Graph
6 Application
6.1 Maximal Matching with Iterated Mediated Population Protocols
6.2 The Simulations
7 Conclusion
References
Constraints
Extending the Notion of Preferred Explanations for Quantified Constraint Satisfaction Problems
1 Introduction
2 Preliminaries
3 Relaxations of Requirements
4 Preferred Conflicts as Explanations
5 Two-Point Relaxation Functions
6 Multi-point Relaxation Functions
7 Totally Ordered Requirement Relaxations
8 Preferences on Requirement Relaxations
9 Checking Equivalence for Partial Implementations
10 Conclusions
References
A Graphical Theorem of the Alternative for UTVPI Constraints
1 Introduction
2 Preliminaries
3 Constraint Network Representation
3.1 Edge Reductions
4 Related Work
5 Theorem of the Alternative: Linear Feasibility
6 Conclusion
References
Logic and Semantic
Converging from Branching to Linear Metrics on Markov Chains
1 Introduction
2 Preliminaries and Notation
3 Markov Chains and Linear-Time Equivalences
4 Trace Distances and Probabilistic Model Checking
5 Convergence from Branching to Linear Distances
5.1 The Strong Case
5.2 The Stutter Case
6 Approximation Schema for the Linear Distances
6.1 The Strong Case
6.2 The Stutter Case
7 Conclusions and Future Work
References
MSO Logic and the Partial Order Semantics of Place/Transition-Nets
1 Introduction
2 Preliminaries
2.1 The Monadic Second Order Logic of Partial Orders
2.2 Petri Nets
2.3 The Causal Semantics of Petri Nets
3 Slice Automata
4 c-Partial-Orders
5 MSO-Definable Sets of c-Partial-Orders and Slice Languages
6 c-Partial-Orders and Petri Nets
6.1 Synthesis
7 Behavioural Design and Correction
7.1 Optimally Correcting Subsystem
7.2 Behavioral Repair
7.3 Synthesis from Partial Order Contracts
8 Conclusion
References
A Resource Aware Computational Interpretation for Herbelin's Syntax
1 Introduction
2 The E-Calculus
3 A Non-idempotent Typing System for E-Terms
4 Characterizing Strongly E-Normalizing Terms
5 The I-Calculus
6 A Non-idempotent Typing System for I-Terms
7 Characterizing Strongly I-Normalizing Terms
8 Conclusion
References
Undecidability Results for Multi-Lane Spatial Logic
1 Introduction
2 Multi-Lane Spatial Logic
2.1 The Model
2.2 The Logic
3 Undecidability of MLSL
3.1 Construction
4 Undecidability of Robust Satisfiability
4.1 Robust Satisfiability of MLSL
4.2 Construction
5 Discussion
6 Conclusion
References
Software Architecture and Component-Based Design
Aspect-Oriented Development of Trustworthy Component-based Systems
1 Introduction
2 The BRIC Component Model
2.1 CSP
2.2 BRIC
3 Aspect Oriented Modelling for BRIC
4 Safely Evolving BRIC Components Using Aspects
5 Case Study
6 Conclusions and Related Work
References
A Game of Attribute Decomposition for Software Architecture Design
1 Introduction
2 Algorithmic Attribute Driven Design (ADD) Process
2.1 Software Requirements and Constraints
2.2 Attribute Primitives
2.3 The ADD Procedure
3 Decomposition Games
3.1 Requirement Relevance
3.2 Decomposition Games
3.3 Solution Concept
4 Solving Decomposition Games
5 Case Study: Cafeteria Ordering System
6 Conclusion and Future Work
References
Multi-rate System Design Through Integrating Synchronous Components
1 Introduction
2 Foundations
2.1 Tagged Model
2.2 Clocked Guarded Actions and Quartz
3 Synthesis of Mode-Based Interface Behaviors
3.1 SMT-based Synthesis of Controlflow-Driven Productions
3.2 Synthesis of Modes and Mode Switching
4 Affine Communications for Multi-mode Components
4.1 Affine Communication Patterns
4.2 Consistent Communication Networks
4.3 Mode-Based Schedules and Buffering Requirements
5 Conclusion
References
Verification
Verifying Android's Permission Model
1 Introduction
2 Background
3 A Formally Verified Security Model of Android
3.1 The Proof Setting
3.2 Model States
3.3 Platform Semantics
4 Security Properties
4.1 Privileges
4.2 Permission Redelegation
5 Related Work
6 Conclusion and Future Work
References
CSP and Kripke Structures
1 Introduction
2 A UTP Theory of Reactive Processes
3 A UTP Theory for Normalised Graphs
4 A UTP Theory for Kripke Structures
5 A UTP Theory for Traces and Maximal Refusals
5.1 Satisfaction for Normalised Graphs
5.2 Satisfaction for Kripke Structures
6 Conclusions
References
Specifying and Analyzing the Kademlia Protocol in Maude
1 Introduction
2 Preliminaries and Related Work
2.1 Maude
2.2 Kademlia
2.3 Related Work
3 Protocol Specification
3.1 Peers
3.2 RPCs
3.3 Process Specification in Maude
4 Centralized Simulation
4.1 First Architecture Abstraction
4.2 Second Architecture Abstraction
4.3 Formal Abstractions
5 Analysis
6 Conclusion and Ongoing Work
References
Enforcement of (Timed) Properties with Uncontrollable Events
1 Introduction
2 Preliminaries and Notation
3 Enforcement Monitoring of Untimed Properties
3.1 Enforcement Functions and their Requirements
3.2 Synthesising Enforcement Functions
3.3 Enforcement Monitors
4 Enforcement Monitoring of Timed Properties
4.1 Enforcement Functions and their Properties
4.2 Synthesising an Enforcement Function
4.3 Enforcement Monitors
4.4 Example
5 Related Work
6 Conclusion and Future Work
References
Tool Papers
A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
1 Introduction
2 Theory
2.1 Semantic Domain
2.2 Conformance
2.3 Test-Case Generation
3 Tool
4 Experiment: DC-DC Boost Converter
5 Conclusions and Future Work
References
CAAL: Concurrency Workbench, Aalborg Edition
1 Introduction
2 Modelling Features
3 Verification Engine
4 Case Study
5 Conclusion
References
A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
1 Introduction
2 Preliminaries
3 Reactive Modules Games
4 Reactive Modules Games in Python
5 Case Study: A Peer-to-Peer Communication Protocol
6 Future Work
References
Short Papers
A Mathematical Game Semantics of Concurrency and Nondeterminism
1 Introduction
2 Concurrent Games as Event Structures
3 Nondeterministic Closure Operators
4 Strategies as Nondeterministic Closure Operators
5 Characterising Winning Strategies
6 Conclusions, Application Domains, and Related Work
References
First Steps Towards Cumulative Inductive Types in CIC
1 Introduction
2 pCIC with Cumulative Inductive Types (pCuIC)
2.1 Typing Rules
2.2 Reduction Rules
2.3 Cumulativity
2.4 Properties
3 Lesser pCuIC
4 Discussion and Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken