Foundations of Software Science and Computation Structures : 26th International Conference, FoSSaCS 2023, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings

This open access book constitutes the proceedings of the 26th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2023, which was held during April 22-27, 2023, in Paris, France, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023. The 26 regular papers presented in this volume were carefully reviewed and selected from 85 submissions. They deal with research on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems. ETAPS Foreword Preface Organization Contents When Programs Have to Watch Paint Dry 1 Introduction 2 Modal Types for Temporal Resources 2.1 (Fitch-Style) Modal Types 2.2 Modal Types for Temporal Resources 3 A Calculus for Programming with Temporal Resources 3.1 Types 3.2 Terms 3.3 Type System 3.4 Admissibility of Renamings and Substitutions 3.5 Equational Theory 4 Denotational Semantics 4.1 Interpretation of Types 4.2 Interpretation of Value and Computation Terms 4.3 Renamings, Substitutions, and Soundness 5 Quotienting Delays 6 Related and Future Work 6.1 Related Work 6.2 Future Work 7 Conclusion References Deciding Contextual Equivalence of v-Calculuswith E ectful Contexts 1 Introduction 2 The mref-calculus and the mv-calculus 3 Operational Game Semantics 3.1 Abstract values 3.3 Interactive LTS 3.4 Typing LTS 3.5 Disclosing LTS 3.6 Operational Game Semantics: LTS and Trace Equivalence 4 Lassen Trees for the mv-calculus 4.1 POGS and POGS bipartite bisimulation 4.2 Bipartite Bisimulations for OGS and POGS 4.3 Deciding pogs 4.4 Relating the Transitions in OGS and POGS 5 Relating Bisimilarities in OGS and POGS 5.1 Up-to techniques for 'ogs 5.2 Properties of the Limit (in OGS) 5.3 Correspondence Between 'ogs and 'pogs 6 Related Work 7 Conclusion References Kantorovich Functors and Characteristic Logicsfor Behavioural Distances 1 Introduction 2 Preliminaries 2.1 Categories and Coalgebras 2.2 Quantales and Quantale-Enriched Categories 2.3 Predicate Liftings 2.4 Quantale-Enriched Relations and Lax Extensions 3 Topological Liftings 3.1 Kantorovich Liftings 3.2 Liftings Induced by Lax Extensions 4 Behavioural Distance 5 Expressivity of Quantitative Coalgebraic Logics 6 Conclusions and Future Work References A Logical Framework withHigher-Order Rational (Circular) Terms 1 Introduction 2 Mixed Inductive and Coinductive Definitions 2.1 Finitely Padded Rational Streams 3 The Type Theory 3.1 Higher-Order Rational Terms 3.2 Syntax 3.3 Trace Condition 3.4 Hereditary Substitution 3.5 Term Equality 3.6 Type Checking Rules 3.7 Metatheorems 4 Encoding Subtyping Systems for Recursive Types 4.1 Encoding a Classical Subtyping System 4.2 Encoding a Polarized Circular Subtyping System forEquirecursive Types 5 Related Work 6 Conclusion References A Higher-Order Language for Markov Kernelsand Linear Operators 1 Introduction 2 Mathematical Preliminaries 3 Syntax 3.1 A Markov Kernel Language 3.2 A Linear Language 3.3 Combining Languages 4 Categorical Semantics 5 Concrete Models 5.1 Discrete Probability 5.2 Continuous Probability 6 Beyond Probability 7 Related Work A Typing Rules and Denotational Semantics LL and MK B Commutative Diagrams C Monoidal Monads and Their Algebras D Proofs References A Formal Logic for Formal Category Theory 1 Introduction 2 Syntax of VETT 2.1 Category Connectives 2.2 Set Connectives 2.3 Type Connectives 3 Formal Category Theory in VETT 4 Semantics 5 Related and Future Work References A Strict Constrained Superposition Calculus forGraphs 1 Introduction 2 Graphs and Graph Operations 2.1 Subgraphs and Replacement 2.2 Graph Merging 3 An Equational Logic on Graphs 4 Superposition Calculus with Uninterpreted Labels 4.1 Inference Rules 4.2 Redundancy 5 A Constrained Graph Superposition Calculus 5.1 Constrained Clauses 5.2 Lifting the Calculus 5.3 Soundness and Refutational Completeness 5.4 Redundancy Testing 6 Conclusion References A Programming Language CharacterizingQuantum Polynomial Time 1 Introduction 2 First-order quantum programming language 3 Polynomial time soundness 4 FBQP completeness 5 Compilation to polynomial-size quantum circuits References On the Existential Arithmetics with Additionand Bitwise Minimum 1 Introduction 2 Definitions and the main example 2.1 Definability and automata 2.2 Existential characterization of k-FA-recognizable languages 3 First-order characterization of Parikh automata 4 Multi-counter machines and DPR-theorem 4.1 Two-way multi-counter machines 4.2 The role of concatenation in DPR-theorem 5 Conclusion References Coverability in 2-VASS with One Unary Counteris in NP ⋆ 1 Introduction 2 Preliminaries 3 Coverability in 2-VASS with One Unary Counter 4 Replacing Short Cycles 5 Reshuffling Linear Form Paths 5.1 Reshuffling Procedure 5.2 Applying Reshuffling 6 Proof of Theorem 1 7 Conclusion and Future Work References On History-Deterministic One-Counter Nets 1 Introduction 2 Preliminaries 3 Deciding History-Determinism 3.1 Token Games 3.2 Lower Bounds 4 Languages and History-Determinism in OCNs 4.1 Languages Accepted by History-Deterministic OCNs 4.2 Complexity of comparing languages of history-deterministicOCNs 5 Extensions and Variations of OCN 5.1 Succinct Encoding of Counters 5.2 Deciding History-Determinsm for OCA 6 Discussion Acknowledgements References Unboundedness Problems for Machines with Reversal-Bounded Counters 1 Introduction 2 Main Results: Unboundedness and (P)RBCA 3 Translating reversal-bounded counters into Z-counters 4 Deciding unboundedness predicates 5 Growth References Reverse Bisimilarity vs. Forward Bisimilarity 1 Introduction 2 The Nondeterministic Case 2.1 Syntax of Nondeterministic Reversible Processes 2.2 Semantics of Nondeterministic Reversible Processes 2.3 Bisimilarities for Nondeterministic Reversible Processes 2.4 Congruence Properties 2.5 Equational Characterizations 3 The Markovian Case 3.1 Markov Chains: Definition, Representation, Terminology 3.2 Time Reversibility of Continuous-Time Markov Chains 3.3 Lumpability of Continuous-Time Markov Chains 3.4 Syntax and Semantics of Markovian Reversible Processes 3.5 Bisimilarities for Markovian Reversible Processes 3.6 Congruence Properties and Equational Characterizations 4 Conclusions Acknowledgments. References Explainability of Probabilistic BisimilarityDistances for Labelled Markov Chains 1 Introduction 1.1 Main Results 1.2 Related Work 2 Labelled Markov Chains and Probabilistic BisimilarityDistances 3 A Logical Characterization 4 All Operators are Necessary 5 Explainability 6 Computing fnst 7 The Algorithm 8 Conclusion References Weighted and Branching Bisimilarities fromGeneralized Open Maps 1 Introduction 2 From Path Categories to Bisimilarity 3 Weighted Bisimilarity and Open Maps 3.1 Larsen-Skou Bisimilarity Using Open Maps 3.2 Impossibility Result for Generative Systems 4 Generalized Open Maps 4.1 Generalized Open Maps Situation 4.2 Basic Properties 5 Open Maps for Weighted Systems 5.1 Category of Coalgebras for Weighted Systems 5.2 Generalized Open Maps Situation for Weighted Systems 5.3 Equivalence between Open Maps and Proper Homomorphisms 5.4 About Sub-distribution Functor 6 Open Maps for Branching Bisimilarity 6.1 LTSs with Internal Moves, Category and Bisimilarities 6.2 Generalized Open Maps for Branching Bisimulations 6.3 Equivalence of Bisimilarities 7 Conclusions and Future Work References Preservation and Reflection of Bisimilarityvia Invertible Steps 1 Introduction 2 Forward and Backward Steps 2.1 Invertible Steps 2.2 Steps from weak liftings, and other examples 3 Relations, Liftings and Coalgebraic Bisimulations 4 Preserving and Reflecting Bisimilarity 4.1 Preservation and reflection 4.2 Proof of preservation and reflection 5 Applications 6 Discussion and Future Work 6.1 Remarks on other notions of bisimulation 6.2 Future work Acknowledgements References Quantitative Safety and Liveness 1 Introduction 2 Quantitative Properties 3 Quantitative Safety 3.1 Alternative Characterizations of Quantitative Safety 3.2 Related Definitions of Quantitative Safety 4 The Quantitative Safety-Progress Hierarchy 4.1 Infimum and Supremum Properties 4.2 Limit Inferior and Limit Superior Properties 5 Quantitative Liveness 5.1 The Quantitative Safety-Liveness Decomposition 5.2 Related Definitions of Quantitative Liveness 6 Approximate Monitoring through Approximate Safety 6.1 The Intersection of Approximate Safety and Co-safety 6.2 Finite-state Approximate Monitoring 7 Conclusion Acknowledgments. References On the Comparison of Discounted-SumAutomata with Multiple Discount Factors 1 Introduction 2 Preliminaries 3 Comparison of NMDAs 3.1 The Reduction 3.2 Undecidability of Comparison 4 Comparison of NDAs with Different Discount Factors 5 Conclusions Acknowledgements References Fast Matching of Regular Patternswith Synchronizing Counting 1 Introduction 2 Preliminaries 3 Counting Automata 4 Counter-subset Construction 5 Fast Simulation of Counting-set Automata 6 Augmented Determinization 7 Regexes with Synchronizing Counting 8 Practical Considerations 8.1 Occurrence of Synchronizing Counting in Practice 8.2 Practical Efficiency of Matching with Synchronizing Counting 9 Conclusions Acknowledgment References Compositional Learning for Interleaving ParallelAutomata 1 Introduction 2 Related Work 3 Preliminaries 3.1 Finite State Machines (FSMs) 3.2 (De)Composing FSMs 3.3 Model Learning 4 Compositional Active Learning 4.1 Termination Analysis 4.2 Processing Counter-examples 5 Empirical Evaluation 5.1 Subject Systems 5.2 Experiment Design 5.3 Results 5.4 Threats to Validity 6 Conclusions Acknowledgments References Pebble minimization: the last theorems 1 Introduction 2 Preliminaries on two-way transducers 3 Blind and last pebble transducers 4 Factorization forests 5 Height minimization of blind pebble transducers 5.1 Pumpability 5.2 Algorithm for removing a recursion layer 6 Height minimization of last pebble transducers 6.1 Pumpability 6.2 Algorithm for removing a recursion layer 7 Making the two last pebbles visible 8 Outlook Acknowledgements References Fixed Points and Noetherian Topologies 1 Introduction 1.1 Contributions of this paper 2 A Quick Primer on Noetherian Topologies 3 Refinements of Noetherian topologies 3.1 An ill-behaved refinement function 3.2 Well-behaved refinement functions 3.3 Iterating Expanders 4 Applications of Topology Expanders 5 Consequences on inductive definitions 5.1 Divisibility Topologies of Analytic Functors 5.2 Divisibility Preorders 6 Outlook References An Efficient Cyclic Entailment Procedure in a Fragmentof Separation Logic 1 Introduction 2 Decidable Fragment SHLIDe 2.1 Separation Logic Formulas 2.2 Semantics 3 Entailment Problem & Overview 3.1 Exclude-the-Middle Proof System 3.2 Cyclic Proofs 4 Cyclic Entailment Procedure 4.1 Proof Search 4.2 Illustrative Example 5 Soundness, Completeness, and Complexity 6 Implementation and Evaluation 7 RelatedWork 8 Conclusion References Just Testing 1 Introduction 2 Labelled Petri nets with read arcs 3 A Petri net semantics of CCSP with signalling 4 Justness and other completeness criteria 5 Feasibility 6 The coarsest preorders preserving linear time properties 7 Congruence properties 8 Must Testing 9 Timed must-testing 10 Conclusion References Model and Program Repair via Group Actions 1 Introduction 1.1 Our Contributions 2 Related Work 2.1 Computation Tree Logic Repair 2.2 Group theoretic model checking 3 Temporal Logic and Kripke Structures 4 Quotient Structures 4.1 Groups Acting on Kripke Structures 4.2 Constructing the Quotient structure 4.3 Semantic Relationships Between Structures and QuotientStructures 5 Repair of Concurrent Programs 5.1 Repair of Symmetry-reduced Structures 5.2 Extraction of Concurrent Programs from Symmetry-reducedStructures 6 Examples 6.1 Two process Mutual Exclusion 6.2 n-Process Mutual Exclusion 6.3 No G-closed Repairs 7 Relative Completeness of Group Theoretic Repair 8 Conclusions References Subgame Optimal Strategies in FiniteConcurrent Games with Prefix- Independent Objectives 1 Introduction 2 Preliminaries 3 Game forms 4 Concurrent games and optimal strategies 4.1 Concurrent arenas and strategies 4.2 More on strategies 5 Necessary and sufficient condition for subgame optimality 6 From subgame almost-surely winning to subgameoptimality 7 Finite-choice strategies References Author Index