ABSTRACT. Probabilistic CTL is obtained from the standard CTL (Computational Tree Logic) by replacing the existential and universalpath quantifiers with the probabilistic operator where the probabilityof runs satisfying a given path formula is bounded by a rationalconstant. We survey the existing results about the satisfiability andvalidity problems for probabilistic CTL, and we also present some of theunderlying proof techniques.

ABSTRACT. Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. We give a detailed overview of today's state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This presentation thereby provides a guide for MDP verification practitioners---tool builders and users alike.

The original Practitioner's Guide to MDP Model Checking Algorithms (https://link.springer.com/chapter/10.1007/978-3-031-30823-9_24) was nominated for a best paper award at TACAS'23. This presentation is based on the revised version of that paper which will be part of the invited special issue of TACAS'23. The intended presenter is M. Weininger.

ABSTRACT. Reachability is a fundamental decision problem that arises across various domains, including program analysis, computational models like cellular automata, and finite- and infinite-state concurrent systems. Mortality, closely related to reachability, is another critical decision problem.

This study focuses on the computational complexity of the reachability and mortality problems for two-dimensional hierarchical piecewise constant derivative systems (2-HPCD) and, consequently, for one-dimensional piecewise affine maps (1-PAM). Specifically, we consider the bounded variants of 2-HPCD and 1-PAM, as they are proven to be equivalent regarding their reachability and mortality properties.

The proofs leverage the encoding of the simultaneous incongruences problem, a known NP-complete problem, into the reachability (alternatively, mortality) problem for 2-HPCD. The simultaneous incongruences problem has a solution if and only if the corresponding reachability (alternatively, mortality) problem for 2-HPCD does not. This establishes that the reachability and mortality problems are co-NP-hard for both bounded 2-HPCD and bounded 1-PAM.

ABSTRACT. This paper introduces Semi-Linear Integer Vector Addition Systems with Resets (SVASR). A SVASR is a labeled transition system in which the states are finite rational-valued vectors and the transitions go from one state to another by applying an orthogonal projection followed by a translation drawn from a semi-linear set. We give a polynomial-time algorithm for computing a linear integer arithmetic formula defining the reachability relation of an SVASR with states and a stack.

We then consider the use of SVASRs for over-approximating the reachability relation of transition systems in which the transition relation is a semi-linear set. We show that any semi-linear transition system has a ``best'' SVASR that simulates its behavior, called its SVASR-reflection. The dimension of the SVASR-reflection of a semi-linear transition system $T$ with states is exponential in the number of states; however, we show that the over-approximate reachability induced by $T$'s SVASR-reflection can be computed in polynomial time.

ABSTRACT. This paper studies the linear recurrence automata model in which multiple linear recurrences can be used to generate sequences of numbers. We parameterised the model by varying several structural properties to identify under which constraints or extensions the reachability problems become computationally hard and undecidable. We show first the reduction of classical matrix semigroup problems to reachability in linear recurrence automata and then analyse several variants of the model restricting the state structures, the number and the depth of recurrences.

ABSTRACT. Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. Extending this paradigm to the quantitative domain, where properties are arbitrary functions mapping infinite words to partially-ordered domains, we introduce and study the notions of quantitative safety and liveness.

First, we formally define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of boolean properties. Consequently, like their boolean counterparts, quantitative properties can be $\min$-decomposed into safety and liveness parts, or alternatively, $\max$-decomposed into co-safety and co-liveness parts.

Second, we instantiate our framework with the specific classes of quantitative properties expressed by automata. These quantitative automata contain finitely many states and rational-valued transition weights, and their common value functions $\Inf$, $\Sup$, $\LimInf$, $\LimSup$, $\LimInfAvg$, $\LimSupAvg$, and $\DSum$ map infinite words into the totally-ordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a $\min$-decomposition into safe and live automata.

ABSTRACT. We propose a new procedure for Metric Interval Temporal Logic (MITL) model checking problem by first providing a translation of MITL formulae to the recently proposed model of generalized timed automata (GTA) and a new zone-based algorithm for checking Büchi non-emptiness in GTAs. Our translation offers an exponential improvement w.r.t. the state-of-the-art translation. An extended version of this work will appear at CONCUR 2024.

ABSTRACT. This paper continues the study of measure-once finite quantum automata building on work by Bertoni, Choffrut et al. and Blondel et al. We investigate conditions ensuring that, given a language recognized by such a device and a language generated by a context-free grammar of finite index or by a matrix context-free grammar, it is decidable whether or not they have a nonempty intersection.  

ABSTRACT. Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS).

Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of *runs* is equipped with a wqo and supports *amalgamation* of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete.

Moreover, this abstract setting enables simple and general algorithmic solutions to *unboundedness problems*, which have received much attention in recent years. We present algorithms for the (i)~simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii)~computing priority downward closures, (iii)~deciding whether a language is bounded, meaning included in $w_1^*\cdots w_k^*$ for some words $w_1,\ldots,w_k$, and (iv)~effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.

This work has been accepted for publication at LICS 2024.

ABSTRACT. In the basic formalism of term rewriting, targets of rewriting are finite terms. On the other hand, in infinitary rewriting, we may consider rewriting of (possibly) infinite terms. Top-down tree transducers, as well as term rewriting, usually deal with transformations of finite terms; we can naturally consider transformations for infinitary terms. We discuss preservation of rationality by top-down tree transducers, namely the problem whether infinite terms reachable by top-down tree transducers from rational terms are rational.

ABSTRACT. We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states.

We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification. For loop-free programs, the MD strategies resulting from our weakest precondition-style framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification.

We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachability-reward objectives.

I will show the applicability of this approach by means of some case studies.

(This is based on joint work with Kevin Batz, Tom Biskup, and Tobias Winkler.)