Accepted Papers and Presentations

Regular Papers

• Alexander Bilgram, Peter Gjøl Jensen, Thomas Pedersen, Jiri Srba and Peter H. Taankvist. Improvements in Unfolding of Colored Petri Nets

  Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analyses in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach remains competitive w.r.t. unfolding time, it outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2020 Model Checking Contest.

• Marco Sälzer and Martin Lange. Reachability Is NP-Complete Even for the Simplest Neural Networks

  We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We repair some flaws in the original upper and lower bound proofs. We then show that NP-hardness already holds for restricted classes of simple specifications and neural networks with just one layer, as well as neural networks with minimal requirements on the occurring parameters.

• Oleg Karpenkov. Continued Fraction approach to Gauss-Reduction theory

  Jordan Normal Forms serve as excellent representatives of conjugacy classes of matrices over closed fields. Once we knows normal forms, we can compute functions of matrices, their main invariant, etc. The situation is more complicated if we search for normal forms for conjugacy classes over fields that are not closed and especially over rings. In this paper we study PGL(2,Z)-conjugacy classes of GL(2,Z) matrices. For the ring of integers Jordan approach has various limitations and in fact it is not effective. The normal forms of conjugacy classes of GL(2,Z) matrices are provided by alternative theory, which is known as Gauss Reduction Theory. We introduce a new techniques to compute reduced forms In Gauss Reduction Theory in terms of the elements of certain continued fractions. Current approach is based on recent progress in geometry of numbers. The proposed technique provides an explicit computation of periods of continued fractions for the slopes of eigenvectors.

• Maria Kosche, Tore Koß, Florin Manea and Stefan Siemer. Absent Subsequences in Words

  An absent factor of a string $w$ is a string $u$ which does not occur as a contiguous substring (a.k.a. factor) inside $w$. We extend this well-studied notion and define absent subsequences: a string $u$ is an absent subsequence of a string $w$ if $u$ does not occur as subsequence (a.k.a. scattered factor) inside $w$. Of particular interest to us are minimal absent subsequences, i.e., absent subsequences whose every subsequence is not absent, and shortest absent subsequences, i.e., absent subsequences of minimal length. We show a series of combinatorial and algorithmic results regarding these two notions. For instance: we give combinatorial characterisations of the sets of minimal and, respectively, shortest absent subsequences in a word, as well as compact representations of these sets; we show how we can test efficiently if a string is a shortest or minimal absent subsequence in a word, and we give efficient algorithms computing the lexicographically smallest absent subsequence of each kind; also, we show how a data structure for answering shortest absent subsequence-queries for the factors of a given string can be efficiently computed.

• Marcelo Forets and Christian Schilling. Reachability of weakly nonlinear systems using Carleman linearization

  In this article we introduce a solution method for a special class of nonlinear initial-value problems using set-based propagation techniques. The novelty of the approach is that we employ a particular embedding (Carleman linearization) to leverage recent advances of high-dimensional reachability solvers for linear ordinary differential equations based on the support function. Using a global error bound for the Carleman linearization abstraction, we are able to describe the full set of behaviors of the system for sets of initial conditions and in dense time.

• Joseph Livesey and Dominik Wojtczak. Minimal Number of Calls in Propositional Protocols

  Gossip protocols are programs that can be used by a group of agents to synchronise what information they have. Namely, assuming each agent holds a secret, the goal of a protocol is to reach a situation in which all agents are experts, i.e., know all secrets. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. In this paper, we investigate in-depth one of the simplest classes of such gossip protocols: propositional gossip protocols, in which whether an agent wants to initiate a call depends only the set of secrets that the agent currently knows. We establish important properties about the order of calls possible in a correct propositional gossip protocol, i.e., a one that terminates in the desired all-expert state. This allows us to solve the following open problem: all correct propositional gossip protocols for n > 4 agents require at least 2n-2 calls in the worst case.

Presentations

• Guillaume Girol, Benjamin Farinier and Sebastien Bardin. Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference

  Note: this work initially appeared at CAV'21. This paper introduces a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 4 existing vulnerabilities, and compare it with standard symbolic execution.

• Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel and David Chemouil. Sound Verification Procedures for Temporal Properties of Infinite-State Systems

  First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. Decidable fragments have recently been exhibited and open the way for tractable verification. However, these fragments are not expressible enough for realistic specifications. In this paper, we propose three abstraction techniques to translate a typical FOLTL specification into two of its decidable fragments. All three abstractions are proved to be sound (the proofs are validated with Coq) and have a high degree of automation. In order to put these techniques into practice, we propose a specification language relying on FOLTL. Our prototype then perform the verification relying on existing model checkers. We successfully verified safety and liveness properties for 8 specifications of distributed systems from the literature.

• Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt and Guillermo Perez. Continuous One-Counter Automata

  We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.

• Ville Salo. Solitaire of independence

  We introduce the solitaire of independence, and ask some questions about it, in particular we state the associated reachability problem and ask about its complexity. We briefly explain the connection to certain invariant measures on TEP subshifts.

• Stefan Kiefer, Pavel Semukhin and Cas Widdershoven. Linear-Time Model Checking Branching Processes

  (Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this problem is in PSPACE, subsuming classical results for transition systems and Markov chains, respectively. The underlying general model-checking algorithm is based on the automata-theoretic approach, using unambiguous Büchi automata.

• Eric Allender, Archit Chauhan and Samir Datta. Depth-First Search in Directed Planar Graphs, Revisited

  TBA

• Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joel Ouaknine, Mahmoud Salamati, Sadegh Soudjani and James Worrell. The Pseudo-Skolem Problem is Decidable

  We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and, surprisingly, the Skolem problem on pseudo-orbits is also decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.

• Joel Day, Pamela Fleischmann, Maria Kosche, Tore Koß, Florin Manea and Stefan Siemer. The Edit Distance to $k$-Subsequence Universality

  A word $u$ is a subsequence of another word $w$ if $u$ can be obtained from $w$ by deleting some of its letters. In the early 1970s, Imre Simon defined the relation $\sim_k$ (called now Simon-Congruence) as follows: two words having exactly the same set of subsequences of length at most $k$ are $\sim_k$-congruent. This relation was central in defining and analysing piecewise testable languages, but has found many applications in areas such as algorithmic learning theory, databases theory, or computational linguistics. Recently, it was shown that testing whether two words are $\sim_k$-congruent can be done in optimal linear time. Thus, it is a natural next step to ask, for two words $w$ and $u$ which are not $\sim_k$-equivalent, what is the minimal number of edit operations that we need to perform on $w$ in order to obtain a word which is $\sim_k$-equivalent to $u$. In this paper, we consider this problem in a setting which seems interesting: when $u$ is a $k$-subsequence universal word. A word $u$ with $\letters(u)=\Sigma$ is called $k$-subsequence universal if the set of subsequences of length $k$ of $u$ contains all possible words of length $k$ over $\Sigma$. As such, our results are a series of efficient algorithms computing the edit distance from $w$ to the language of $k$-subsequence universal words. In other words, we are interested in optimally editing a word

• Pawel Gawrychowski, Florin Manea and Stefan Siemer. Matching Patterns with Variables under Hamming Distance

  A pattern $\alpha$ is a string of variables and terminal letters. We say that $\alpha$ matches a word $w$, consisting only of terminal letters, if $w$ can be obtained by replacing the variables of $\alpha$ by terminal words. The matching problem, i.e., deciding whether a given pattern matches a given word, was heavily investigated: it is NP-complete in general, but can be solved efficiently for classes of patterns with restricted structure. In this paper, we approach this problem in a generalized setting, by considering approximate pattern matching under Hamming distance. More precisely, we are interested in what is the minimum Hamming distance between $w$ and any word $u$ obtained by replacing the variables of $\alpha$ by terminal words. Firstly, we address the class of regular patterns (in which no variable occurs twice) and propose efficient algorithms for this problem, as well as matching conditional lower bounds. We show that the problem can still be solved efficiently if we allow repeated variables, but restrict the way the different variables can be interleaved according to a locality parameter. However, as soon as we allow a variable to occur more than once and its occurrences can be interleaved arbitrarily with those of other variables, even if none of them occurs more than once, the problem becomes intractable.

• Sebastian Junges, Hazem Torfah and Sanjit A. Seshia. Runtime Monitoring for Markov Decision Processes

  We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk, e.g., the probability of an imminent crash. During runtime, we obtain partial information about the system state in form of observations. The monitor uses this information to estimate the risk of the (unobservable) current system state. Our results are threefold. First, we show that extensions of state estimation approaches do not scale due the combination of nondeterminism and probabilities. While convex hull algorithms improve the practical runtime, they do not prevent an exponential memory blowup. Second, we present a tractable algorithm based on model checking conditional reachability probabilities. Third, we provide prototypical implementations and manifest the applicability of our algorithms to a range of benchmarks. The results highlight the possibilities and boundaries of our novel algorithms. The paper has been presented at CAV 2021, the full paper with appendices can be found at https://arxiv.org/abs/2105.12322. No PDF is attached. For this audience, we would highlight the connection to a formulation as a conditional reachability