Theoretical aspects of computing - ICTAC 2015 : 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings / edited by Martin Leucker, Camilo Rueda, Frank D. Valencia.

This book constitutes the refereed proceedings of the 12th International Colloquium on Theoretical Aspects of Computing, ICTAC 2015 held in Cali, Colombia, in October 2015. The 25 revised full papers presented together with 7 invited talks, 3 tool papers, and s short papers were carefully reviewed and selected from 93 submissions. The papers cover various topics such as algebra and category theory; automata and formal languages; concurrency; constraints, logic and semantic; software architecture and component-based design; and verification.

English.

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 Vertices5.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 Paper2 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 Computations5.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