Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes ω-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic ω-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of ω-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an ω-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of ω-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) – a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.

In adaptive systems, predictors are used to anticipate changes in the system’s state or behavior that may require system adaption, e.g., changing its configuration or adjusting resource allocation. Therefore, the quality of predictors is crucial for the overall reliability and performance of the system under control. This paper studies predictors in systems exhibiting probabilistic and non-deterministic behavior modelled as Markov decision processes (MDPs). Main contributions are the introduction of quantitative notions that measure the effectiveness of predictors in terms of their average capability to predict the occurrence of failures or other undesired system behaviors. The average is taken over all memoryless policies. We study two classes of such notions. One class is inspired by concepts that have been introduced in statistical analysis to explain the impact of features on the decisions of binary classifiers (such as precision, recall, f-score). Second, we study a measure that borrows ideas from recent work on probability-raising causality in MDPs and determines the quality of a predictor by the fraction of memoryless policies under which (the set of states in) the predictor is a probability-raising cause for the considered failure scenario.

Abstract We introduce $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation allows the use of different tolerances for the transition probabilities ( $$\varepsilon $$ ε , additive) and total exit rates ( $$\delta $$ δ , multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for $$(\varepsilon,\delta)$$ ( ε , δ ) -bisimilar states, are established.

To improve reliability and the understanding of AI systems, there is increasing interest in the use of formal methods, e.g. model checking. Model checking tools produce a counterexample when a model does not satisfy a property. Understanding these counterexamples is critical for efficient debugging, as it allows the developer to focus on the parts of the program that caused the issue. To this end, we present a new technique that ascribes a responsibility value to each state in a transition system that does not satisfy a given safety property. The value is higher if the non-deterministic choices in a state have more power to change the outcome, given the behaviour observed in the counterexample. For this, we employ a concept from cooperative game theory – namely general power indices, such as the Shapley value – to compute the responsibility of the states. We present an optimistic and pessimistic version of responsibility that differ in how they treat the states that do not lie on the counterexample. We give a characterisation of optimistic responsibility that leads to an efficient algorithm for it and show computational hardness of the pessimistic version. We also present a tool to compute responsibility and show how a stochastic algorithm can be used to approximate responsibility in larger models. These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems.

Abstract State-of-the-art Probabilistic Model Checking (PMC) offers multiple engines for the quantitative analysis of Markov Decision Processes (MDPs), including rewards modeling cost or utility values. Despite the huge amount of internally computed information, support for debugging and facilities that enhance the understandability of PMC models and results are very limited. As a first step to improve on that, we present the basic principles of PMC-VIS, a tool that supports the exploration of large MDPs together with the computed PMC results per MDP-state through interactive visualization. By combining visualization techniques, such as node-link diagrams and parallel coordinates, with quantitative analysis capabilities, PMC-VIS supports users in gaining insights into the probabilistic behavior of MDPs and PMC results and enables different ways to explore the behaviour of schedulers of multiple target properties. The usefulness of PMC-VIS is demonstrated through three different application scenarios.

Abstract The concept of features provides an elegant way to specify families of systems. Given a base system, features encapsulate additional functionalities that can be activated or deactivated to enhance or restrict the base system’s behaviors. Features can also facilitate the analysis of families of systems by exploiting commonalities of the family members and performing an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. Most prominent, the concept of features has been successfully applied to describe and analyze (software) product lines. We present the toolProFeatthat supports the feature-oriented engineering process for stochastic systems by probabilistic model checking. To describe families of stochastic systems,ProFeatextends models for the prominent probabilistic model checkerPrismby feature-oriented concepts, including support for probabilistic product lines with dynamic feature switches, multi-features and feature attributes.ProFeatprovides a compact symbolic representation of the analysis results for each family member obtained byPrismto support, e.g., model repair or refinement during feature-oriented development. By means of several case studies we show howProFeateases family-based quantitative analysis and compare one-by-one and all-in-one analysis approaches.

The paper reports on first steps towards a systematic design process that ensures quantitative stochastic requirements like requirements on the expected energy consumption or resilience requirements by construction. The idea is to automatically extract a formal model from a configurable system and to use formal analysis techniques to automatically determine a configuration such that the system meets the quantitative requirements. As a proof of concept we present a tool that supports the automated synthesis of protocol parameters for IPC (interprocess communication). The tool takes as input a Lua script describing the communication structure of several processes. This script is annotated with quantitative information such as error probabilities and timing information. The output is a Markov chain specified in the input language of the prominent probabilistic model checker PRISM. This Markov chain yields the basis for quantitative formal analysis of failure scenarios caused by hardware faults in IPC channels. The results yield the basis for finding optimal values for protocol parameters that tune, e.g., the level of resiliency. As an initial demonstration of the tool, we analyze and adjust system parameters of a simple scenario with a few communicating processes and report on results. Though achieved under simplified assumptions, the results presented here are a proof-of-concept towards the vision of automated system configuration.

Conventional approaches for parallel composition of stochastic systems relate probability measures of the individual components in terms of product measures. Such approaches rely on the assumption that components interact stochastically independent, which might be too rigid for modeling real world systems. In this paper, we introduce a parallel-composition operator for stochastic transition systems that is based on couplings of probability measures and does not impose any stochastic assumptions. When composing systems within our framework, the intended dependencies between components can be determined by providing so-called spans and span couplings. We present a congruence result for our operator with respect to a standard notion of bisimilarity and develop a general theory for spans, exploiting deep results from descriptive set theory. As an application of our general approach, we propose a model for stochastic hybrid systems called stochastic hybrid motion automata.

In controller synthesis, i.e., the question whether there is a controller or strategy to achieve some objective in a given system, the controller is often realized as some kind of automaton. In the context of the exogenous coordination language Reo, where the coordination glue code between the components is realized as a network of channels, it is desirable for such synthesized controllers to also take the form of a Reo connector built from a repertoire of basic channels. In this paper, we address the automatic construction of such Reo connectors directly from a constraint automaton representation.