Cover Image

Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings.

Bibliographic Details
Main Author: Bouyer, Patricia.
Other Authors: Schröder, Lutz.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2022.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • ETAPS Foreword
  • Preface
  • Organization
  • Parameterized Verification to the Rescue of Distributed Algorithms (Abstract of Invited Talk)
  • Contents
  • Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 NFAs, UFAs, DFAs, NBAs, UBAs, SUBAs, and DBAs
  • 2.2 LTL formulas
  • 2.3 M2MAs
  • 2.4 Size lower bounds for DFAs, M2MAs and NFAs
  • 3 M2MAs as representations of regular languages
  • 3.1 M2MAs: procedures for operations and properties
  • 3.2 Conciseness comparisons for regular languages
  • 4 Representing regular omega-languages using regularlanguages
  • 5 Conciseness comparisons for regular omega-languages
  • 5.1 Size increases for LTL formulas
  • 5.2 Size increases for DBAs, NBAs, SUBAs
  • 6 Empirical results
  • 6.1 SUBAs to minimized M2MAs and DFAs
  • 6.2 NBAs and DBAs to minimized M2MAs
  • 6.3 LTL formulas to minimized M2MAs
  • 7 Summary and conclusions
  • References
  • Limits and difficulties in the design of under-approximation abstract domains
  • 1 Introduction
  • 2 Background
  • 3 Integer Domains
  • 3.1 Infinite Integer Domain
  • 3.2 Finite Integer Domain
  • 4 Arbitrary domains
  • 4.1 Local Requirements for Impossibility
  • 4.2 Global Requirements for Impossibility
  • 5 On the necessity of high surjectivity hypothesis
  • 6 Conclusions and Future Works
  • References
  • On probability-raising causality in Markov decision processes
  • 1 Introduction
  • 2 Preliminaries
  • 3 Strict and global probability-raising causes
  • 3.1 Examples and simple properties of probability-raising causes
  • 3.2 Related work
  • 4 Checking the existence of PR causes and the PR conditions
  • 4.1 Checking the strict probability-raising condition and the existence of causes
  • 4.2 Checking the global probability-raising condition
  • 5 Quality and optimality of causes.
  • 5.1 Quality measures for causes
  • 5.2 Computation schemes for the quality measures for fixed cause set
  • 5.3 Quality-optimal probability-raising causes
  • 6 Conclusion
  • References
  • Parameterized Analysis of Reconfigurable Broadcast Networks
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Multisets
  • 2.2 Reconfigurable Broadcast Networks
  • 2.3 Cubes and Counting Sets
  • 3 Reachability sets of counting sets
  • 3.1 Symbolic graph
  • 3.2 Properties of the symbolic graph
  • 4 The PSPACE Theorem
  • 5 Application 1: Almost-sure coverability
  • 5.1 The almost-sure coverability problem
  • 5.2 A characterization of almost-sure coverability
  • 5.3 PSPACE-completeness of the almost-sure coverability problem
  • 6 Application 2: Computation by RBN
  • 6.1 RBN Protocols
  • 6.2 Expressivity
  • References
  • Separators in Continuous Petri Nets
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Separators and bi-separators
  • 3 A characterization of unreachability
  • 4 Separators as certificates
  • 4.1 Locally closed bi-separators
  • 5 Constructing locally closed bi-separators
  • 6 Checking locally closed bi-separators is in NC
  • 7 Bi-separators for set-to-set unreachability
  • 8 Conclusion
  • References
  • Graphical Piecewise-Linear Algebra
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Props and Symmetric Monoidal Theories
  • 2.2 Ordered Props and Symmetric Monoidal Inequality Theories
  • 2.3 Graphical Polyhedral Algebra
  • 3 Symmetric Monoidal Semi-Lattice Theories
  • 4 The Theory of Piecewise-Linear Relations
  • 4.1 Syntax and Semantics
  • 4.2 Equational Theory
  • 4.3 Completeness Theorem
  • 5 Generating Piecewise-Linear Relations
  • 5.1 The n-Fold Union Generators
  • 5.2 The Simplest Non-Convex Diagram
  • 5.3 The Semantics of a Diode
  • 5.4 Alternative generators: max, ReLu and abs
  • 5.5 Conclusion
  • 6 Case Study: Electronic Circuits
  • References.
  • Token Games and History-Deterministic Quantitative Automata
  • 1 Introduction
  • 2 Preliminaries
  • 3 Token Games
  • 4 Deciding History-Determinism via One-Token Games
  • 5 Deciding History-Determinism via Two Token Games
  • 5.1 G₂ on LimSup and LimInf Automata
  • 5.2 G₂ Characterises HDness for LimSup and LimInf Automata
  • 6 Conclusions
  • Acknowledgments
  • References
  • On the Translation of Automatato Linear Temporal Logic
  • 1 Introduction
  • 2 Preliminaries
  • 3 Unary Alphabet
  • 4 General Alphabet
  • 4.1 Cascaded Automata
  • 4.2 Encoding Reachability within Reset Cascades by LTL Formulas
  • 4.3 Depth and Length Analysis
  • 4.4 Translating Deterministic Counter-Free Automata to LTL
  • 5 Conclusions
  • References
  • Categorical composable cryptography
  • 1 Introduction
  • 1.1 Related work
  • 2 Resource theories
  • 3 Cryptography as a resource theory
  • 4 Computational security
  • 5 Applications
  • 6 Outlook
  • References
  • DyNetKAT: An Algebra of Dynamic Networks
  • 1 Introduction
  • 2 Language Design
  • 2.1 Brief Overview of NetKAT
  • 2.2 Design Decisions
  • 2.3 DyNetKAT Syntax
  • 2.4 DyNetKAT Semantics
  • 3 Semantic Results
  • 4 A Framework for Safety
  • 5 Implementation
  • 6 Experimental Evaluation
  • 7 Conclusions
  • References
  • A new criterion for M, N-adhesivity, with an application to hierarchical graphs
  • 1 Introduction
  • 2 M,N-adhesivity via creation of (co)limits
  • 2.1 M, N-adhesive categories
  • 2.2 A new criterion for M, N-adhesivity
  • 2.3 Comma categories
  • 3 Some paradigmatic examples
  • 3.1 Directed (acyclic) graphs
  • 3.2 Tree Orders
  • 3.3 Various kinds of hierarchical graphs
  • 4 Conclusions
  • References
  • Quantifier elimination for counting extensions of Presburger arithmetic
  • 1 Introduction
  • 2 Presburger arithmetic with counting quantifiers
  • 3 A quantifier elimination procedure for PAC.
  • 4 Discussion, summary of results and roadmap
  • 5 The monadically-guarded fragment of PAC
  • 6 Eliminating monadically-guarded counting quantifiers
  • 7 The monadically-guarded fragment is in doubly exponential space
  • 8 A complexity characterisation
  • 9 Conclusion
  • References
  • A first-order logic characterisation of safety and co-safety languages
  • 1 Introduction
  • 2 Preliminaries
  • 3 Safety-FO and coSafety-FO
  • 4 Safety-FO captures LTL-definable safety languages
  • 5 Conclusions
  • References
  • First-order separation over countable ordinals
  • 1 Introduction
  • 2 Preliminaries
  • 2.1 Ordinals
  • 2.2 Ordinal words
  • 2.3 Ordinal monoids
  • 2.4 First-order logic
  • 3 The algorithm
  • 3.1 The saturation construction
  • 3.2 The algorithm
  • 4 When the algorithm says 'no'
  • 5 When the algorithm says 'yes'
  • 5.1 Merge operators and FO-approximants
  • 5.2 Construction of FO-approximants for words of finite andω-length
  • 5.3 Construction of FO-approximants for countable ordinal words
  • 6 Related problems
  • 7 Conclusion
  • References
  • A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications
  • 1 Introduction
  • 2 A Calculus with Generalized Applications
  • 2.1 Syntax and Semantics
  • 2.2 Towards a Call-by-Name Operational Semantics
  • 2.3 Some (Un)typed Properties of λJ
  • 3 Inductive Characterization of Strong Normalization
  • 3.1 ISN in the λ-Calculus Through Weak-Head Contexts
  • 3.2 ISN for dβ
  • 4 Quantitative Types Characterize Strong Normalization
  • 4.1 The Typing System
  • 4.2 The Characterization of dβ-Strong Normalization
  • 4.3 Why π Is Not Quantitative
  • 5 Faithfulness of the Translation
  • 5.1 Explicit Substitutions
  • 5.2 Proof of Faithfulness
  • 6 Equivalent Notions of Strong Normalization
  • 6.1 β-Normalization Is Not Enough
  • 6.2 Comparison with β + p2
  • 6.3 Comparison with β + π.
  • 6.4 Consequences for ΛJ
  • 7 Conclusion
  • References
  • Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy
  • 1 Introduction
  • 2 Preliminaries
  • 3 Lower bounds for ML(9kFO) and ML(9kSO)
  • 4 Upper bounds via a small-model property for ML(9kSO)
  • 5 Further connections
  • References
  • Temporal Stream Logic modulo Theories
  • 1 Introduction
  • 2 Preliminaries
  • 3 Temporal Stream Logic modulo Theories
  • 3.1 Temporal Stream Logic
  • 3.2 Extending TSL with Theories
  • 4 TSL modulo TU Satisfiability Checking
  • 4.1 Buchi Stream Automata
  • 4.2 An Algorithm for TSL modulo TU Satisfiability Checking
  • 5 Undecidability of TSL modulo TU Satisfiability
  • 6 (Semi-)Decidable Fragments
  • 7 Evaluation
  • 8 Related Work
  • 9 Conclusion
  • References
  • The Different Shades of Infinite Session Types
  • 1 Introduction
  • 2 Shades of types
  • 3 Types, trees and traces
  • 4 From types to automata
  • 5 From automata to types
  • 6 Related work
  • 7 Conclusion
  • References
  • Complete and tractable machine-independent characterizations of second-order polytime
  • 1 Introduction
  • 2 A second-order language with imperative procedures
  • 3 Type system
  • 4 Characterizations of the class of Basic Feasible Functionals
  • 5 A completeness-preserving termination criterion
  • 6 Conclusion and future work
  • References
  • Variable binding and substitution for (nameless) dummies
  • 1 Introduction
  • 2 De Bruijn monads
  • 2.1 Definition of De Bruijn monads
  • 2.2 Lifting assignments
  • 2.3 Binding arities and binding conditions
  • 2.4 Binding signatures and algebras
  • 3 Initial-algebra semantics of binding signatures in De Bruijn monads
  • 3.1 A category of De Bruijn monads
  • 3.2 Categories of De Bruijn algebras
  • 4 Relation to presheaf-based models
  • 4.1 Trimming down presheaf-based models
  • 4.2 Trimming down De Bruijn monads.
  • 4.3 Bridging the gap.

Similar Items