Related papers: Model-Checking PCTL Properties of Stateless Probab…

Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type…

Computing the reachability probability in infinite state probabilistic models has been the topic of numerous works. Here we introduce a new property called \emph{divergence} that when satisfied allows to compute reachability probabilities…

Standpoint linear temporal logic ($SLTL$) is a recently introduced extension of classical linear temporal logic ($LTL$) with standpoint modalities. Intuitively, these modalities allow to express that, from agent $a$'s standpoint, it is…

This paper presents a probabilistic model validation methodology for nonlinear systems in time-domain. The proposed formulation is simple, intuitive, and accounts both deterministic and stochastic nonlinear systems with parametric and…

In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of…

We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or…

The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of…

Probabilistic model checking is an approach to the formal modelling and analysis of stochastic systems. Over the past twenty five years, the number of different formalisms and techniques developed in this field has grown considerably, as…

(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…

We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems.

The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable.…

This paper presents a novel approach for augmenting proof-based verification with performance-style analysis of the kind employed in state-of-the-art model checking tools for probabilistic systems. Quantitative safety properties usually…

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of reactive probabilistic systems. We explore XPL, an extension to GPL allowing the semantics of nondeterminism present in…

We study termination time and recurrence time in programs with unbounded recursion, which are either randomized or operate on some statistically quantified inputs. As the underlying formal model for such programs we use probabilistic…

In this paper, we evaluate the capability of transformer-based language models in making inferences over uncertain text that includes uncertain rules of reasoning. We cover both Pre-trained Language Models (PLMs) and generative Large…

We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata…

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for…

In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central importance. Traditionally, such requirements have been…

Transaction-level modeling with SystemC has been very successful in describing the behavior of embedded systems by providing high-level executable models, in which many of them have inherent probabilistic behaviors, e.g., random data and…

There are several forms of irreducibility in computing systems, ranging from undecidability to intractability to nonlinearity. This paper is an exploration of the conceptual issues that have arisen in the course of investigating speed-up…