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 / edited by Patricia Bouyer, Lutz Schröder.

Format:

Book

Author/Creator:

Bouyer, Patricia, Editor.

Contributor:

Bouyer, Patricia, 1976-

Schröder, Lutz.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 13242

Language:

English

Subjects (All):

Computer science.

Logic, Symbolic and mathematical.

Data structures (Computer science).

Information theory.

Computer systems.

Computer science--Mathematics.

Theory of Computation.

Mathematical Logic and Foundations.

Data Structures and Information Theory.

Computer System Implementation.

Mathematics of Computing.

Local Subjects:

Theory of Computation.

Mathematical Logic and Foundations.

Data Structures and Information Theory.

Computer System Implementation.

Mathematics of Computing.

Physical Description:

1 online resource (xvi, 471 pages) : illustrations.

Edition:

1st ed. 2022.

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2022.

Language Note:

English

Summary:

This open access book constitutes the proceedings of the 25th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2022, which was held during April 4-6, 2022, in Munich, Germany, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022. The 23 regular papers presented in this volume were carefully reviewed and selected from 77 submissions. They deal with research on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems. .

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

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

On probability-raising causality in Markov decision processes

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

Parameterized Analysis of Reconfigurable Broadcast Networks

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

Separators in Continuous Petri Nets

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

Graphical Piecewise-Linear Algebra

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

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

On the Translation of Automatato Linear Temporal Logic

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

Categorical composable cryptography

1.1 Related work

2 Resource theories

3 Cryptography as a resource theory

4 Computational security

5 Applications

6 Outlook

DyNetKAT: An Algebra of Dynamic Networks

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

A new criterion for M, N-adhesivity, with an application to hierarchical graphs

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

Quantifier elimination for counting extensions of Presburger arithmetic

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

A first-order logic characterisation of safety and co-safety languages

3 Safety-FO and coSafety-FO

4 Safety-FO captures LTL-definable safety languages

First-order separation over countable ordinals

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

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications

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

Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy

3 Lower bounds for ML(9kFO) and ML(9kSO)

4 Upper bounds via a small-model property for ML(9kSO)

5 Further connections

Temporal Stream Logic modulo Theories

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

The Different Shades of Infinite Session Types

2 Shades of types

3 Types, trees and traces

4 From types to automata

5 From automata to types

6 Related work

Complete and tractable machine-independent characterizations of second-order polytime

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

Variable binding and substitution for (nameless) dummies

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.

Notes:

Includes author index.

Description based upon print version of record.

ISBN:

3-030-99253-5

OCLC:

1308973551