Theoretical Aspects of Computing – ICTAC 2023 : 20th International Colloquium, Lima, Peru, December 4–8, 2023, Proceedings

This book constitutes the proceedings of the 20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023, which took place in Lima, Peru, during December 4–8, 2023. The 20 full papers presented in this volume together with 3 invited papers and 1 tool paper were carefully reviewed and selected from 40 submissions. They were organised in the topical sections as follows: Bring Together Practitioners; Researchers from Academia; Industry; Government to Present Research Results and Exchange Experience and Ideas. Preface Organization Contents Optimal Route Synthesis in Space DTN Using Markov Decision Processes References Without Loss of Satisfaction 1 Introduction 2 Background 3 Mutilated chessboards 4 Mycielski graphs 5 Ramsey numbers References Modelling and Verifying Robotic Software that Uses Neural Networks 1 Introduction 2 Background 2.1 ANNs 2.2 CSP and UTP 3 Modelling ANN Components in RoboChart 4 CSP Semantics 5 Automated Verification Using UTP 5.1 General Pattern 5.2 Cyclic Memoryless RoboChart Controllers 5.3 Conformance 6 Conclusions References A Game-Theoretic Approach to Indistinguishability of Winning Objectives as User Privacy 1 Introduction 2 Preliminaries 3 Multiple Nash Equilibrium 4 Indistinguishable Strategy and Related Equilibrium 5 Decidability Results 6 Conclusion References Learning Attack Trees by Genetic Algorithms 1 Introduction 1.1 Related Work 2 Background 2.1 Attack Trees 2.2 Attack Trees vs Decision Trees 3 Genetic Algorithm for Learning ADT 3.1 Fitness Function 3.2 Mutations and Crossovers for Attack Trees 3.3 Extension to Attack-Defense Trees 4 Experiments 4.1 Generating Input Datasets 4.2 Sanity Check: Perfect Fitting for Small Models 4.3 Crossvalidation: No Overfitting of Models 4.4 Comparison to Logistic Regression 4.5 Learning Attack Trees 4.6 Hyperparameter Optimization 4.7 Real-World Demonstration: KDD Cup 1999 Dataset 5 Conclusion and Future Work References The Landscape of Computing Symmetric n-Variable Functions with 2n Cards 1 Introduction 2 Symmetric Boolean Functions 3 Existing Protocols 3.1 Two Variables 3.2 Three Variables 3.3 Four Variables 3.4 More Than Four Variables 4 Our Protocol for kMod3 Function 4.1 Preliminaries 4.2 Encoding Integers in Z/3Z 4.3 Adding Two Commitments in Z/3Z 4.4 Adding Two Integers in Z/3Z 4.5 Main Protocol 4.6 Proof of Correctness and Security 4.7 Analysis 5 Future Work References On the Complexity of Reasoning in Kleene Algebra with Commutativity Conditions 1 Introduction 2 Proof Idea 3 Encoding of Looping 4 Effective Inseparability Argument References Towards the Complexity Analysis of Programming Language Proof Methods 1 Introduction 2 Operational Semantics and Complexity Definitions 3 Analysis of Canonical Form Lemmas 4 Analysis of the Progress Theorem 4.1 Analysis of the Main Theorem 4.2 Analysis of Operator-Specific Progress Theorems 5 Analysis of the Type Preservation Theorem 6 Limitations of Our Analysis 7 Related Work 8 Conclusion References A Dynamic Temporal Logic for Quality of Service in Choreographic Models 1 Introduction 2 Related Work 3 Preliminaries 4 Quality of Service of Communicating Systems 5 QL: A Dynamic Logic for QoS 6 A Semidecision Procedure for QL 6.1 A Bounded Model-Checking Approach for QL 7 Conclusions References Interactive Matching Logic Proofs in Coq 1 Introduction 2 Matching Logic 2.1 Matching Logic Syntax 2.2 Matching Logic Semantics 2.3 Definedness, Totality, Equality 2.4 The Hilbert-Style Proof System 3 A Single-Conclusion Sequent Calculus 3.1 Proof Constraints 3.2 Sequents 3.3 Meta-properties of S 4 Implementation of the Proof Mode 4.1 Matching Logic Proof System in Coq 4.2 Example Interactive Proof 4.3 Proof Constraints 4.4 Architecture of the Proof Mode 5 Evaluation 5.1 First-Order Proofs 5.2 Rewriting-Based Proofs 5.3 Complex Proofs 6 Related Work 7 Conclusion References An Autonomous Data Language 1 Introduction 2 Concepts and Motivating Example 3 Syntax 4 Semantics 5 Standard Algorithms 5.1 Creating a Spanning Tree 5.2 Sorting 6 Related Work 7 Conclusion References Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling 1 Introduction 2 Background 2.1 Statecharts 2.2 Run-to-Completion and SCXML 2.3 Event-B 3 Turnstile Example 4 Formalization of Untriggered Statecharts 4.1 Formalization of the Untriggered Statechart Syntactic Elements 4.2 Formalization of the Untriggered Statechart Semantics 5 Formalization of the Run-to-Completion Schedule 5.1 Formalization of the Run-to-completion Syntactic Elements 5.2 Formalization of the Run-to-Completion Semantics 6 Formalization of Triggered Statecharts 6.1 Triggered Statechart Syntactic Elements 6.2 Triggered Statechart Semantics 7 Conclusions References Strong Call-by-Value and Multi Types 1 Introduction 2 Technical Preliminaries 3 Call-by-Value and Call-by-Fireball 4 Value Substitution Calculus 5 The External Strategy 6 Multi Types by Value 7 Multi Types for Open CbV 8 Shrinking Multi Types for the External Strategy 9 Conclusions References Algorithms for Checking Intersection Non-emptiness of Regular Expressions 1 Introduction 2 Preliminaries 2.1 Regular Expressions and Deterministic Regular Expressions 2.2 Position Automaton and Star Normal Form 2.3 Derivatives of Regular Expressions 3 Position-Based Algorithms 4 C-Continuation-Based Algorithms 5 Experimental Evaluation 6 Related Work 7 Concluding Remarks References Realisability of Global Models of Interaction 1 Introduction 2 Formal Preliminaries 3 SpecifyingRequirementsforGlobalModelsofInteraction 4 Realisations of Global Models of Interaction 4.1 Realisations Using Rich Local Actions 4.2 Realisations Using Poor Local Actions 5 Realisability Conditions 5.1 Condition for Realisability Using Rich Local Actions 5.2 Condition for Realisability Using Poor Local Actions 6 Tool Support: Ceta 7 Conclusion References Efficient Reactive Synthesis Using Mode Decomposition 1 Introduction 2 Motivating Example 3 Preliminaries 4 Mode Based Synthesis 4.1 Mode Based Decomposition 4.2 The Mode-Base Projection Algorithm MoBy 4.3 Composing Solutions 5 Empirical Evaluation 6 Conclusion and Future Work References A Categorical Approach to Synthetic Chemistry 1 Introduction 2 Retrosynthetic Analysis 3 Layered Props 4 Chemical Graphs 5 Disconnection Rules 6 Reactions 7 Retrosynthesis in Layered Props 8 Discussion and Future Work References Closure and Decision Properties for Higher-Dimensional Automata 1 Introduction 2 Pomsets with Interfaces 3 Higher-Dimensional Automata 4 Regular and Non-regular Languages 5 ST-Automata 6 Complement 7 Conclusion and Further Work References Robustness in Metric Spaces over Continuous Quantales and the Hausdorff-Smyth Monad 1 Mathematical Preliminaries 2 Quantales 2.1 Continuous Quantales 3 Quantale-Valued Metric Spaces 4 Topologies on Q-Metric Spaces 4.1 Imprecision and Robustness 5 Separation in Preorder-Enriched Categories 6 The Hausdorff-Smyth Monad 6.1 Hausdorff-Smyth and *-Robust Topology 7 Concluding Remarks References Synchronous Agents, Verification, and Blame—A Deontic View 1 Introduction 2 Preliminaries 3 A Deontic Logic for Collaboration 3.1 Informative Semantics 3.2 Blame Assignment 3.3 Quantitative Semantics 4 Analysis 4.1 Contracts to Automata 4.2 Model Checking 4.3 Blame Assignment 5 Related Work 6 Conclusions References Store Locally, Prove Globally 1 Introduction 2 Memories 3 A Distributed Process Calculus with Local Memories 4 Location Failures and Their Detection 5 Case Study: Distributed Consensus 6 Conclusion A Definitions References Denotational Semantics for Symbolic Execution 1 Introduction 2 The Language While 3 Symbolic Execution Semantics 4 Symbolic Execution 4.1 Final Substitutions 4.2 Path Conditions 4.3 Direct Symbolic Execution 5 Extension to Procedure Calls 5.1 Concrete Semantics 5.2 Symbolic Semantics 5.3 Symbolic Execution Traces 6 Related Work 7 Conclusions and Future Work References TeSSLa-ROS-Bridge – Runtime Verification of Robotic Systems 1 Introduction 2 Preliminaries 3 TeSSLa-ROS-Bridge 4 TeSSLa-ROS-Bridge in Action 5 Conclusions and Future Work References Simplifying Process Parameters by Unfolding Algebraic Data Types 1 Introduction 2 Motivating Example 3 Preliminaries 3.1 Data 3.2 Linear Processes 4 Parameter Unfolding 4.1 Extending the Data Specification 4.2 Unfolding Process Parameters in an LPE 5 Improving Parameter Unfolding 5.1 Alternative Case Placement 5.2 Global Variables 5.3 Simplifications for Pattern Matching Rules 6 Experiments 7 Conclusion References Modular Soundness Checking of Feature Model Evolution Plans 1 Introduction 2 Background 2.1 Software Product Lines 2.2 Planning Feature Model Evolution 2.3 Spatial and Temporal Scopes of Update Operations 3 Formalisation of IBFMs 4 Soundness 4.1 Well-Formedness of Interval-Based Feature Models 4.2 Soundness of the Rule System 5 Related Work 6 Conclusion A Helper Functions ch25thesis References Author Index