View: session overviewtalk overview
09:00 | The Satisfiability and Validity Problems for Probabilistic CTL 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. |
10:00 | The Revised Practitioner's Guide to MDP Model Checking Algorithms PRESENTER: Maximilian Weininger 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. |
14:00 | Safety and Liveness of Quantitative Properties and Automata 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. |
14:15 | MITL Model Checking via Generalized Timed Automata and a new Liveness Algorithm 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. |
14:30 | Quantum automata and languages of finite index 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. |
15:00 | Verifying Unboundedness via Amalgamation PRESENTER: Lia Schütze 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. |
15:15 | Preservation of Rationality in Infinitary Rewriting by Top-Down Tree Transducers 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. |
We meet at 5:30pm (sharp!) at the Tram STOP KARLSPLATZ in front of the Otto Wagner - Pavillon, for a Vintage Tram Tour in Vienna, visiting the historical places in Vienna and going to Grinzing.
Dinner is at 7pm in Heuriger Bio-Weinbau & Heurigenschank „ZUM BERGER“ Himmelstrasse 19 A – 1190 Wien.