Neural networks are increasingly important to learn action policies. Policy predicate abstraction (PPA) verifies safety of such a neural policy pi by over-approximating the state space subgraph induced by pi and using counterexample-guided abstraction refinement (CEGAR) to iteratively refine the abstraction. So far, PPA verifies safety in non-deterministic systems. This work extends PPA to probabilistic verification. Extending the abstract state space computation is relatively straightforward. Abstraction refinement, however, becomes substantially more complex, due to the more intricate form of counterexamples and the various sources of spuriousness it entails. We tackle this challenge by drawing inspiration from prior work on probabilistic CEGAR, empowering it to deal with neural pi. The resulting algorithm decides whether pi is safe with respect to a desired upper bound on unsafety probability. Invoking the algorithm incrementally, we can also derive upper and lower bounds automatically. Our experiments show that these algorithms can derive non-trivial bounds, whereas encodings into state-of-the-art probabilistic model checkers turn out to be ineffective.

Explainable AI (XAI) is crucial for building transparent and trustworthy machine learning systems, especially in high-stakes domains. Concept Bottleneck Models (CBMs) have emerged as a promising ante-hoc approach that provides interpretable, concept-level explanations by explicitly modeling human-understandable concepts. However, existing CBMs often suffer from poor locality faithfulness, failing to spatially align concepts with meaningful image regions, which limits their interpretability and reliability. In this work, we propose SL-CBM (CBM with Semantic Locality), a novel extension that enforces locality faithfulness by generating spatially coherent saliency maps at both concept and class levels. SL-CBM integrates a 1 × 1 convolutional layer with a cross-attention mechanism to enhance alignment between concepts, image regions, and final predictions. Unlike prior methods, SL-CBM produces faithful saliency maps inherently tied to the model’s internal reasoning, facilitating more effective debugging and intervention. Extensive experiments on image datasets demonstrate that SL-CBM substantially improves locality faithfulness, explanation quality, and intervention efficacy while maintaining competitive classification accuracy. Our ablation studies highlight the importance of contrastive and entropy-based regularization for balancing accuracy, sparsity, and faithfulness. Overall, SL-CBM bridges the gap between concept-based reasoning and spatial explainability, setting a new standard for interpretable and trustworthy concept-based models.

Abstract A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the $$\texttt {{\textbf {AnyMiss}}}\,(2, 300)$$ AnyMiss ( 2 , 300 ) weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures. Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45 k states for $$\texttt {{\textbf {AnyMiss}}}\,(2, 300)$$ AnyMiss ( 2 , 300 ) ) is a notorious impediment for the verification of control system properties. This paper discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.

In 2026, we saw rising numbers of proposals for orbital data centers to facilitate AI, e.g., by SpaceX (up to one million satellites), Blue Origin, and Google—yet none include rigorous lifecycle sustainability analysis. We present ESpaS-ODC, a lifecycle carbon model that accounts for the three subsystems physically unavoidable at GPU-class power densities but absent from prior work: a thermal radiator sized from ISS data, solar-array degradation and eclipse margin, and cold-standby spares for no-repair access. Applying the model to an edge data center in a 510 km orbit reveals that the service-overhead-scaled radiator weighs about eleven times the GPU it serves and that modeled power and thermal infrastructure dominate launched component mass—not compute. Using mission duration T as the denominator to amortize launch, re-entry, and manufacturing carbon, model-boundary parity with a global-average terrestrial DC occurs within the first two mission years in our parameter sweep. With respect to a renewables-powered green-energy DC (Finland grid intensity: 68 gCO2e/kWh, PUE: 1.2), parity requires multi-year missions with cold-standby spares compensating the shorter component lifetimes. Idealized dawn-dusk SSO (no-eclipse regime, β > βcrit) eliminates the eclipse battery, cutting modeled component mass significantly (e.g., 25% on the 1 kW-ODC for a 3 yr mission), but leaves the radiator unchanged: high-beta orbits solve the battery problem, not the thermal problem. Finally, carrying one full cold spare (r = 2) increases amortized carbon per GPU hour by 40% on Starship and 34% on Falcon-9 at T = 3 yr, while its dependability benefit remains to be quantified.

Abstract This article introduces a framework that is meant to assist in mitigating societal risks that software can pose. Concretely, this encompasses facets of software doping as well as unfairness and discrimination in high-risk decision-making systems. The term software doping refers to software that contains surreptitiously added functionality that is against the interest of the user. A prominent example of software doping are the tampered emission cleaning systems that were found in millions of cars around the world when the diesel emissions scandal surfaced. The first part of this article combines the formal foundations of software doping analysis with established probabilistic falsification techniques to arrive at a black-box analysis technique for identifying undesired effects of software. We apply this technique to emission cleaning systems in diesel cars but also to high-risk systems that evaluate humans in a possibly unfair or discriminating way. We demonstrate how our approach can assist humans-in-the-loop to make better informed and more responsible decisions. This is to promote effective human oversight, which will be a central requirement enforced by the European Union’s upcoming AI Act. We complement our technical contribution with a juridically, philosophically, and psychologically informed perspective on the potential problems caused by such systems.

Abstract Decision diagrams (DDs) are an important data structure in computer science with applications ranging from circuit design and verification to machine learning. Most prominently, binary DDs are commonly used to succinctly represent Boolean functions. Due to the practical importance of DDs, there is an ongoing quest for high-performance software libraries supporting the construction and manipulation of DDs. With OxiDD, we present a new framework for DDs that focuses on safety, concurrency, and modularity. Following a highly modular design we implement OxiDD in Rust, which facilitates the integration of various kinds of DDs such as MTBDDs, ZBDDs, and TDDs, all within safe code also in a concurrent setting. Already in its initial release, OxiDD does not compromise performance, which we show to be on par with or even better than established highly optimized DD libraries.

Abstract This paper is about shipping runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild. Concretely, we present an Android app that deploys rtlola runtime monitors for the purpose of diagnosing automotive exhaust emissions. For this, it harvests the availability of cheap Bluetooth adapters to the On-Board-Diagnostics (obd) ports, which are ubiquitous in cars nowadays. The app is a central piece in a set of tools and services we have developed for black-box analysis of automotive vehicles. We detail its use in the context of real driving emission (rde) tests and report on sample runs that helped identify violations of the regulatory framework currently valid in the European Union.

Abstract Neural networks (NN) are taking over ever more decisions thus far taken by humans, even though verifiable system-level guarantees are far out of reach. Neither is the verification technology available, nor is it even understood what a formal, meaningful, extensible, and scalable testbed might look like for such a technology. The present paper is an attempt to improve on both the above aspects. We present a family of formal models that contain basic features of automated decision-making contexts and which can be extended with further orthogonal features, ultimately encompassing the scope of autonomous driving. Due to the possibility to model random noise in the decision actuation, each model instance induces a Markov decision process (MDP) as verification object. The NN in this context has the duty to actuate (near-optimal) decisions. From the verification perspective, the externally learnt NN serves as a determinizer of the MDP, the result being a Markov chain which as such is amenable to statistical model checking. The combination of an MDP and an NN encoding the action policy is central to what we call “deep statistical model checking” (DSMC). While being a straightforward extension of statistical model checking, it enables to gain deep insight into questions like “how high is the NN-induced safety risk?”, “how good is the NN compared to the optimal policy?” (obtained by model checking the MDP), or “does further training improve the NN?”. We report on an implementation of DSMC inside the Modest Toolset in combination with externally learnt NNs, demonstrating the potential of DSMC on various instances of the model family, and illustrating its scalability as a function of instance size as well as other factors like the degree of NN training.

Online fault diagnosis techniques are a key enabler of effective failure mitigation. For real-time systems, the problem of identifying faults is aggravated by timing imprecisions such as varying latency between events and their observation. This paper tackles the challenge of diagnosing faults based on partial observations which are subject to timing imprecisions and potentially made out-of-order due to latency. In this paper, we develop a theory of robust real-time diagnosis importing well-established notions from timed automata theory and the diagnosis of discrete event systems. The theory itself enables a foundational understanding and investigation of the problem and its intricacies. Based on this theory, we further devise an online diagnosis algorithm consuming observations incrementally as they are made and enabling diagnosis, whenever possible, within a bounded worst-case delay. We prove the correctness of the algorithm and its properties with respect to the theory. Aiming at practical feasibility, we also show how to obtain sound but not necessarily complete diagnosis results with space and time requirements bounded by the size of the system model and independent of the number of observations. Finally, using a prototypical implementation, we report on first empirical results obtained by simulation of a small excerpt of an industrial automation example.

Abstract M o G ym , is an integrated toolbox enabling the training and verification of machine-learned decision-making agents based on formal models, for the purpose of sound use in the real world. Given a formal representation of a decision-making problem in the JANI format and a reach-avoid objective, M o G ym (a) enables training a decision-making agent with respect to that objective directly on the model using reinforcement learning (RL) techniques, and (b) it supports rigorous assessment of the quality of the induced decision-making agent by means of deep statistical model checking (DSMC). M o G ym implements the standard interface for training environments established by OpenAI Gym, thereby connecting to the vast body of existing work in the RL community. In return, it makes accessible the large set of existing JANI model checking benchmarks to machine learning research. It thereby contributes an efficient feedback mechanism for improving in particular reinforcement learning algorithms. The connective part is implemented on top of Momba. For the DSMC quality assurance of the learned decision-making agents, a variant of the statistical model checker modes of the M odest T oolset is leveraged, which has been extended by two new resolution strategies for non-determinism when encountered during statistical evaluation.

Abstract Software doping is a phenomenon that refers to the presence of hidden software functionality, whose existence is only in the interest of the manufacturer. The most prominent example is the diesel emissions scandal. There is a need for methods that identify software doping, and such methods are bound to be applied to the final product with no or rare knowledge about its internals. Black-box analysis techniques have recently been developed for this purpose, harvesting the formal foundations of software doping. This paper integrates them with established falsification techniques for the purpose of real-world applicability. With a focus on the diesel scandal and emissions tests on chassis dynamometers we make the testing procedures significantly more effective in terms of time and cost. The theoretical results are implemented in a prototypical doping tester.

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion for classical reasoning in abstract argumentation frameworks, it has barely been reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of abstract argumentation based on probabilistic notions of admissibility. Our approach follows the natural idea of defining probabilistic semantics for abstract argumentation by systematically imposing constraints on the joint probability distribution on the sets of arguments, rather than on probabilities of single arguments. As a result, there might be either a uniquely defined distribution satisfying the constraints, but also none, many, or even an infinite number of satisfying distributions are possible. We provide probabilistic semantics corresponding to the classical complete and stable semantics and show how labeling schemes provide a bridge from distributions back to argument labelings. In relation to existing work on probabilistic argumentation, we present a taxonomy of semantic notions. Enabled by the constraint-based approach, standard reasoning problems for probabilistic semantics can be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation.

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Abstract State-of-the-art program-analysis techniques are not yet able to effectively verify safety properties of heterogeneous systems, that is, systems with components implemented using diverse technologies. This shortcoming is pinpointed by programs invoking neural networks despite their acclaimed role as innovation drivers across many application areas. In this paper, we embark on the verification of system-level properties for systems characterized by interaction between programs and neural networks. Our technique provides a tight two-way integration of a program and a neural-network analysis and is formalized in a general framework based on abstract interpretation. We evaluate its effectiveness on 26 variants of a widely used, restricted autonomous-driving benchmark.

Direct-to-Satellite IoT allows devices on the Earth surface to directly reach Low-Earth Orbit (LEO) satellites passing over them. Although an appealing approach towards a truly global IoT vision, scalability issues as well as highly dynamic topologies ask for dedicated protocol adaptations supported by novel models. This paper contributes to this research by introducing estimators and a transmission probability function to dynamically control the contending set of devices on a framed slotted Aloha model compatible with the LoRaWAN specification. In particular, we discuss techniques that account for particularities in the dynamics of sparse DtS-IoT constellations. Simulation analyses of a realistic case study show that >86% of the theoretical throughput is achievable in practice.

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics, and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion in the classical setting, it has been merely reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of argumentation based on probabilistic notions of admissibility in a way that they form fully conservative extensions of classical notions. In particular, our building blocks are not the beliefs regarding single arguments. Instead we start from the fairly natural idea that whatever argumentation semantics is to be considered, semantics systematically induces constraints on the joint probability distribution on the sets of arguments. In some cases there might be many such distributions, even infinitely many ones, in other cases there may be one or none. Standard semantic notions are shown to induce such sets of constraints, and so do their probabilistic extensions. This allows them to be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation. We present a taxonomy of semantic notions, also in relation to published work, together with a running example illustrating our achievements.

Cyber-physical systems are notoriously hard to verify due to the complex interaction between continuous physical behavior and discrete control. A widespread and important class is formed by digital controllers that operate on fixed control cycles to interact with the physical environment they are embedded in. This paper presents a case study for integrating such controllers into a rigorous verification method for cyber-physical systems, using flowpipe-based verification methods to verify legally binding requirements for electrified vehicles to a custom bike design. The controller is integrated in the underlying model in a way that correctly represents the input discretization performed by any digital controller.

Abstract This paper is about shipping runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild. Concretely, we present an Android app that deploys rtlola runtime monitors for the purpose of diagnosing automotive exhaust emissions. For this, it harvests the availability of cheap bluetooth adapters to the On-Board-Diagnostics (obd) ports, which are ubiquitous in cars nowadays. We detail its use in the context of Real Driving Emissions (rde) tests and report on sample runs that helped identify violations of the regulatory framework currently valid in the European Union.

Abstract JANI-model [6] is a model interchange format for networks of interacting automata. It is well-entrenched in the quantitative model checking community and allows modeling a variety of systems involving concurrency, probabilistic and real-time aspects, as well as continuous dynamics. Python is a general purpose programming language preferred by many for its ease of use and vast ecosystem. In this paper, we presentMomba, a flexible Python framework for dealing with formal models centered around the JANI-model format and formalism. Momba strives to deliver an integrated and intuitive experience for experimenting with formal models making them accessible to a broader audience. To this end, it provides a pythonic interface for model construction, validation, and analysis. Here, we demonstrate these capabilities.

It is widely known that AI planning and model checking are closely related. Compilations have been devised between various pairs of language fragments. What has barely been voiced yet, though, is the idea to let go of one's own modeling language, and use one from the other area instead. We advocate that idea here – to use automata-network languages from model checking instead of PDDL – motivated by modeling difficulties relating to planning agents surrounded by exogenous agents in complex environments. One could, of course, address this by designing additional extended planning languages. But one can also leverage decades of work on modeling in the formal methods community, creating potential for deep synergy and integration with their techniques as a side effect. We believe there's a case to be made for the latter, as one modeling alternative in planning among others.

This short article announces the recipients of the CONCUR Test-of-Time Award 2020.

Abstract We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time– and value–domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Deep neural networks (DNNs) have been applied in safety-critical domains such as self driving cars, aircraft collision avoidance systems, malware detection, etc. In such scenarios, it is important to give a safety guarantee to the robustness property, namely that outputs are invariant under small perturbations on the inputs. For this purpose, several algorithms and tools have been developed recently. In this paper, we present PRODeep, a platform for robustness verification of DNNs. PRODeep incorporates constraint-based, abstraction-based, and optimisation-based robustness checking algorithms. It has a modular architecture, enabling easy comparison of different algorithms. With experimental results, we illustrate the use of the tool, and easy combination of those techniques.

Markov decision processes are of major interest in the planning community as well as in the model checking community. But in spite of the similarity in the considered formal models, the development of new techniques and methods happened largely independently in both communities. This work is intended as a beginning to unite the two research branches. We consider goal-reachability analysis as a common basis between both communities. The core of this paper is the translation from Jani, an overarching input language for quantitative model checkers, into the probabilistic planning domain definition language (PPDDL), and vice versa from PPDDL into Jani. These translations allow the creation of an overarching benchmark collection, including existing case studies from the model checking community, as well as benchmarks from the international probabilistic planning competitions (IPPC). We use this benchmark set as a basis for an extensive empirical comparison of various approaches from the model checking community, variants of value iteration, and MDP heuristic search algorithms developed by the AI planning community. On a per benchmark domain basis, techniques from one community can achieve state-ofthe-art performance in benchmarks of the other community. Across all benchmark domains of one community, the performance comparison is however in favor of the solvers and algorithms of that particular community. Reasons are the design of the benchmarks, as well as tool-related limitations. Our translation methods and benchmark collection foster crossfertilization between both communities, pointing out specific opportunities for widening the scope of solvers to different kinds of models, as well as for exchanging and adopting algorithms across communities.

Size and weight limitations of low-earth orbit (LEO) small satellites make their operation rest on a fine balance between solar power infeed and power demands of communication technologies on board, buffered by on-board battery storage. As a result, the problem of planning battery-powered payload utilization together with intersatellite communication is extremely intricate. Nevertheless, there is a growing trend toward constellations and megaconstellations that are to be managed using sophisticated software support. Earlier work has leveraged cost-optimal reachability in priced timed automata for deriving near-optimal finite-horizon schedules to operate a single LEO satellite in orbit. This article harvests that work and improves it in several dimensions, all needed for true in-orbit applicability: 1) the battery representation is no longer bound to be linear, but can be kinetic, which means that the optimization problem includes nonlinearities; 2) the management is perpetuated by a receding horizon scheduling strategy; 3) the model is continuously improved with the latest telemetry received from orbit; 4) a tandem of satellites equipped with state-of-the-art intersatellite link transponders is considered; 5) the core optimization problem is now solved using dynamic programming with antichain-based pruning, which is proven to be optimal and despite all the additional features outperforms the earlier approach by orders of magnitude; 6) the entire approach is grounded in the concrete requirements of the GOM X-4 LEO mission; 7) care is taken to make the approach usable by the space engineers, and robust against failures of parts of the toolchain; and 8) an extensive test campaign validates accuracy, efficiency, scalability, and robustness with respect to the operational requirements and constraints of LEO constellations.

Abstract When working with space systems the keyword is resources. For a satellite in orbit all resources are scarce and the most critical resource of all is power. It is therefore crucial to have detailed knowledge on how much power is available for an energy harvesting satellite in orbit at every time—especially when in eclipse, where it draws its power from onboard batteries. The challenge is to maximise operational performance of a satellite, while providing hard guarantees that critically low battery levels are avoided, taking into account these power restrictions. Classic approaches to workload scheduling and analysis are not suitable, because of heterogeneity, interdependencies and system dynamics involved. This paper addresses this problem by a two-step procedure to perform task scheduling for low-earth-orbit satellites exploiting formal methods. It combines time-bounded cost-optimal reachability analyses of priced timed automata networks with a realistic kinetic battery model capable of capturing capacity limits as well as stochastic fluctuations. We also discuss how the time-bounded analysis can be embedded into a workflow that exploits in-orbit current and voltage measurements so as to perpetuate the task scheduling. The core procedure has been exercised in-orbit for the automatic and resource-optimal day-ahead scheduling of G om X–3, a power-hungry 3-unit nanosatellite. We explain how this approach has overcome existing problems, has led to improved designs, and has provided new insights.

Power demands of the transmission technologies for communication between LEO satellites are difficult to counterbalance by solar infeed and on-board battery storage, due to size and weight limitations in LEO. This makes the problem of battery-powered inter-satellite communication a very difficult one. Its management requires a profound understanding as well as techniques for a proper extrapolation of the electric power budget as part of the inter-satellite and satellite-to-ground communication design. We discuss how the construction of contact plans in delay tolerant networking can profit from a sophisticated model of the on-board battery behaviour. This model accounts for both nonlinearities in battery behaviour as well as stochastic fluctuations in charge, so as to control the risk of battery depletion. We take an hypothetical Ulloriaq constellation based on the GomX-4 satellites from GomSpace as a reference for our studies.

Emission cleaning in modern cars is controlled by embedded software. In this context, the diesel emission scandal has made it apparent that the automotive industry is susceptible to fraudulent behaviour, implemented and effectuated by that control software. Mass effects make the individual controllers altogether have statistically significant adverse effects on people’s health. This paper surveys recent work on the use of rigorous formal techniques to attack this problem. It starts off with an introduction into the dimension and facets of the problem from a software technology perspective. It then details approaches to use (i) model checking for the white-box analysis of the embedded software, (ii) model- based black-box testing to detect fraudulent behaviour under standardized conditions, and (iii) synthesis of runtime monitors for real driving emissions of cars in-the-wild. All these efforts aim at finding ways to eventually ban the problem of doped software, that is, of software that surreptitiously alters its behaviour in certain circumstances – against the interest of the owner or of society.

The Internet of Things (IoT) is announced to swamp the world. In order to understand the emergent behaviour of connected things, effective support for the modelling of connection and failure probabilities, execution and waiting times, as well as resource consumptions of various kinds is needed. At the heart of IoT are flexible and adaptive communication and interaction patterns between things, meant to enable advanced as well as radically new emerging functionalities. Since these interaction patterns are determined by topological characteristics, they can naturally be modelled by channel-based exogenous coordination primitives. In this paper, we tackle the IoT modelling challenge. Our modelling approach is based on a conservative extension of Reo circuits. On a technical level, we work with a model called Priced Probabilistic Timed Constraint Automaton, which combines existing models of probabilistic and timed aspects, and is equipped with pricing information. The latter enables us to reason about resource consumption, especially important in light of severely limited power, memory and computation budgets in things. The approach is set up in such a way that the original constituent models can be retrieved without changes in syntax and semantics. A small but illustrative IoT case is modelled and evaluated, demonstrating the principal benefits of the proposed approach.

The EnergyBus specification is the basis of an ongoing joint IEC/ISO standardisation effort focussing on public charging infrastructures for and interoperability of light electric vehicle components. This paper highlights how these efforts are supported by formal methods, starting at the design and specification level, up to establishing a certification framework for standards compliance of devices implementing the specification. The Modest Toolset supports the model-based analysis methods needed in this context.

Abstract Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.

Scenario-aware dataflow is a formalism to model modern dynamic embedded applications whose behaviour is heavily dependent on input data or the operational environment. Key behavioural aspects are the execution times and energy consumption of a system's components. In this paper, we introduce flexible scenario-aware dataflow: a proper generalisation of previous definitions that allows any execution time to be specified as discretely or continuously random or nondeterministic. Additionally, it supports the modelling of abstract costs like the energy usage of components. We give a formal compositional semantics in terms of networks of stochastic timed automata. We have implemented support for analysing performance properties of flexible scenario-aware dataflow graphs via simulation and model checking. A number of reduction techniques are applied to make the underlying state spaces tractable for model checking. We evaluate the scalability and performance of our new model and implementation on standard benchmarks.

This invited talk starts off with a review of probabilistic safety assessment (PSA) methods currently exercised across the nuclear power plant domain worldwide. It then elaborates on crucial aspects of the Fukushima Dai-ichi accident which are not considered properly in contemporary PSA studies. New kinds of PSA are needed so as to take into account external hazards, dynamic aspects of accident progression, and partial information. All of these come with obvious increases in algorithmic analysis complexity. This motivates our ongoing work to gradually tackle the resulting modelling and analysis problems. They revolve around static and dynamic fault trees, open interpretations of compositional Markov models and advances in their effective numerical analysis.

Abstract Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.

We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on non-probabilistic programs. The framework is proven sound and complete for a meaningful class of programs involving randomization and bounded nondeterminism. We complement this foundational insigh by a practical proof methodology, based on sound conditions that enable compositional reasoning and are amenable to a direct implementation using modern theorem provers. This is integrated in a small dependent type system, to overcome the problem that lexicographic ranking functions fail when combined with randomization. Among others, this compositional methodology enables the verification of probabilistic programs outside the complete class that admits ranking supermartingales.

Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation, and also branching probabilistic bisimulation. We furthermore present several extensions to interesting related problems, in particular weak and branching probabilistic simulation, setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.

We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of reliability analysis, e.g., of computer network performability analysis, of power grids, of computer virus vulnerability, and in the study of crowd dynamics. We use abstraction techniques together with novel algorithms for the computation of bounds on the expected final and accumulated rewards in continuous-time Markov decision processes (CTMDPs). These ingredients are combined in a partly symbolic and partly explicit (symblicit) analysis approach. In particular, we circumvent the use of multi-terminal decision diagrams, because the latter do not work well if facing a large number of different rates. We demonstrate the practical applicability and efficiency of the approach on two case studies.

Abstraction refinement techniques in probabilistic model checking are prominent approaches for verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This article proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.

The joint consideration of randomness and continuous time is important for the formal verification of many real systems. Considering both facets is especially important for wireless sensor networks, distributed control applications, and many other systems of growing importance. Apart from proving the quantitative safety of such systems, it is important to analyze properties related to resource consumption (energy, memory, bandwidth, etc.) and properties that lie more on the economical side (monetary gain, the expected time or cost until termination, etc.). This paper provides a framework to decide such reward properties effectively for a generic class of models which have a discrete-continuous behaviour and involve both probabilistic as well as nondeterministic decisions. Experimental evidence is provided demonstrating the applicability of our approach.

This paper gives a bird's-eye view of the various ingredients that make up a modern, model-checking-based approach to performability evaluation: Markov reward models, temporal logics and continuous stochastic logic, model-checking algorithms, bisimulation and the handling of non-determinism. A short historical account as well as a large case study complete this picture. In this way, we show convincingly that the smart combination of performability evaluation with stochastic model-checking techniques, developed over the last decade, provides a powerful and unified method of performability evaluation, thereby combining the advantages of earlier approaches.

This paper surveys well-established/recent tools and techniques developed for the design of rigorous embedded systems. We will first survey UPPAAL and MODEST, two tools capable of dealing with both timed and stochastic aspects. Then, we will overview the BIP framework for modular design and code generation. Finally, model-based testing will be discussed.

Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.

Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation. We also present several extensions to interesting related problems setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.

Dealing with the interplay of randomness and continuous time is important for the formal verification of many real systems. Considering both facets is especially important for wireless sensor networks, distributed control applications, and many other systems of growing importance. An important traditional design and verification goal for such systems is to ensure that unsafe states can never be reached. In the stochastic setting, this translates to the question whether the probability to reach unsafe states remains tolerable. In this paper, we consider stochastic hybrid systems where the continuous-time behaviour is given by differential equations, as for usual hybrid systems, but the targets of discrete jumps are chosen by probability distributions. These distributions may be general measures on state sets. Also non-determinism is supported, and the latter is exploited in an abstraction and evaluation method that establishes safe upper bounds on reachability probabilities. To arrive there requires us to solve semantic intricacies as well as practical problems. In particular, we show that measurability of a complete system follows from the measurability of its constituent parts. On the practical side, we enhance tool support to work effectively on such general models. Experimental evidence is provided demonstrating the applicability of our approach on three case studies, tackled using a prototypical implementation.

Assume we have a network of discrete-time Markov decision processes (MDPs) which synchronize via common actions. We investigate how to compute probability measures in case the structure of some of the component MDPs (so-called blackbox MDPs) is not known. We then extend this computation to work on networks of MDPs that share integer data variables of finite domain. We use a protocol which spreads information within a network as a case study to show the feasibility and effectiveness of our approach.

Wireless communication, hard real time requirements and safety criticality do not go together well. This paper reports on the modelling, design, simulation, implementation and deployment of a small exemplary case that possesses all these features. State-of-the-art verification and simulation means are employed to ensure its proper operation.

The European STREP project Quasimodo1 develops theory, techniques and tool components for handling quantitative constraints in model-driven development of real-time embedded systems, covering in particular real-time, hybrid and stochastic aspects. This tutorial highlights the advances made, focussing on real industrial case studies tackled.

We develop a compositional behavioural model that integrates a variation of probabilistic automata into a conservative extension of interactive Markov chains. The model is rich enough to embody the semantics of generalised stochastic Petri nets. We define strong and weak bisimulations and discuss their compositionality properties. Weak bisimulation is partly oblivious to the probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the standard way to associate a stochastic process to a generalised stochastic Petri net can be proven sound with respect to weak bisimulation.

The European electricity market is rapidly evolving towards a decentralized structure, not only because of climatical and political circumstances. The increase of production based on renewable energy implies drastically higher fluctuations in available electricity. This paper introduces the stochastic energy balancing problem, which is a result of these current trends. We sketch IT-supported strategies to counteract this problem, and derive principal considerations for modelling and analysis techniques to assist in the solution of this problem.

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.

Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like Statemate support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of Statemate enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.

As levels of parallelism are becoming increasingly complex in multiprocessor architectures GALS and asynchronous circuits, methodologies and software tools are needed to verify their functional behavior (qualitative properties) and to predict their performance (quantitative properties). This paper presents the work currently done in the multival project (pole de competitivite mondial Minalogic), in which verification and performance evaluation tools developed at INRIA and Saarland University are applied to three industrial architectures designed by Bull CEA/Leti and STMicroelectronics.

Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation over probabilistic automata are not efficient, which makes it as yet unclear whether they can be used as effectively as their non-probabilistic counterparts. This paper presents drastically improved algorithms to decide whether some (discrete- or continuous-time) Markov chain strongly or weakly simulates another, or whether a probabilistic automaton strongly simulates another. The key innovation is the use of parametric maximum flow techniques to amortize computations. We also present a novel algorithm for deciding strong probabilistic simulation preorders on probabilistic automata, which has polynomial complexity via a reduction to an LP problem. When extending the algorithms for probabilistic automata to their continuous-time counterpart, we retain the same complexity for both strong and strong probabilistic simulations.

Continuous-time Markov decision processes (CTMDPs) are behavioral models with continuous-time, nondeterminism and memoryless stochastics. Recently, an efficient timed reachability algorithm for CTMDPs has been presented, allowing one to quantify, e. g., the worst-case probability to hit an unsafe system state within a safety critical mission time. This algorithm works only for uniform CTMDPs -- CTMDPs in which the sojourn time distribution is unique across all states. In this paper we develop a compositional theory for generating CTMDPs which are uniform by construction. To analyze the scalability of the method, this theory is applied to the construction of a fault-tolerant workstation cluster example, and experimentally evaluated using an innovative implementation of the timed reachability algorithm. All previous attempts to model-check this seemingly well-studied example needed to ignore the presence of nondeterminism, because of lacking support for modelling and analysis.

This paper presents Modest (MOdeling and DEscription language for Stochastic Timed systems), a formalism that is aimed to support (i) the modular description of reactive system's behaviour while covering both (ii) functional and (iii) nonfunctional system aspects such as timing and quality-of-service constraints in a single specification. The language contains features such as simple and structured data types, structuring mechanisms like parallel composition and abstraction, means to control the granularity of assignments, exception handling, and non-deterministic and random branching and timing. Modest can be viewed as an overarching notation for a wide spectrum of models, ranging from labeled transition systems, to timed automata (and probabilistic variants thereof) as well as prominent stochastic processes such as (generalized semi-)Markov chains and decision processes. The paper describes the design rationales and details of the syntax and semantics.

Functional Interface (AFI). Models and solution techniques interact with one another through the use of the standard interface, allowing them to interact with M OBIUS framework components, not formalism components. This permits novel combinations of modeling techniques. The AFI uses abstract classes to implement the framework components. The most basic model in the M OBIUS framework is an atomic model, and is made up of state variables that hold information about the state of a model and actions that are used for changing model state. Stochastic activity networks (SANs) and the stochastic process algebra PEPA are example atomic models that have been successfully implemented in the M OBIUS tool.

This paper investigates the tradeoff between reliability and effectiveness for the IPv4 Zeroconf protocol, proposed by Cheshire/Adoba/Guttman in 2002, dedicated to the selfconfiguration of IP network interfaces. We develop a simple stochastic cost model of the protocol, where reliability is measured in terms of the probability to avoid an address collision after configuration, while effectiveness is viewed as the average penalty perceived by a user. We derive an analytical expression for the user penalty which we use to derive optimal configuration parameters of the network, restricting to those parameters which are under the control of a consumer electronics manufacturer. In particular we show that minimal cost and maximal reliability are qualities that cannot be achieved at the same time.

analysis and/or numerical engine. The Analysis engine supports standard model checking algorithms for CTL-style until-formulas, as well as graph algorithms, for instance to compute the bottom strongly connected components of a Markov chain. The former algorithms are used in a pre-processing phase during the checking of probabilistic until-formulas while the latter is needed when calculating steady state properties. The Numerical engine provides several methods for the numerical analysis of the CTMC such as linear solvers, methods for numerical integration and uniformisation. These are used to solve sytems of linear or integral equations. The State space manager represents the model in sparse matrix format. It maintains information about the validity of atomic propositions and of sub-formulas for each state. Status and Availability ETMCC has been used successfully in several non-trivial case studies, e.g. a cyclic server polling system and a multiprocessor mainframe with software failures. Its efficient numerical analysis methods enable users to check performability properties for models of up to several millions of states. The tool is available free of charge for academia, see http://www7.informatik.uni-erlangen.de/etmcc/ ,t he current download being version 1.4. A detailed description of ETMCC can be found in [4].

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.

Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained fairly cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

Stochastic Process Algebras (SPA) are process algebras in which the duration of each activity is given by a random variable. If the stochastic aspect is restricted to Markovian, i.e. exponentially distributed durations, nice algebraic foundations are available. They include a formal semantics and an equational theory for Markovian bisimulation, a congruence that can be seen as a stochastic counterpart of strong bisimulation. This paper extends that theory with a stochastic notion of Milner's observational congruence. We enrich a basic SPA with immediate actions that happen instantaneously if enabled. For the enriched calculus we will derive a sound and complete characterisation of Markovian observational congruence, a conservative extension of both Markovian bisimulation and observational congruence. The usefulness of immediate actions together with their equational theory will be illustrated by means of an example. Additionally, we will discuss some implementation and modelling issues arising from our results.