1,721,009 research outputs found
Probabilistic Semantics: Metric and Logical Character¨ations for Nondeterministic Probabilistic Processes
Full text linkIn this thesis we focus on processes with nondeterminism and probability in the PTS model, and we propose novel techniques to study their semantics, in terms of both classic behavioral relations and the more recent behavioral metrics.
Firstly, we propose a method for decomposing modal formulae in a probabilistic extension of the Hennessy-Milner logic. This decomposition method allows us to derive the compositional properties of probabilistic (bi)simulations.
Then, we propose original notions of metrics measuring the disparities in the behavior of processes with respect to (decorated) trace and testing semantics.
To capture the differences in the expressive power of the metrics we order them by the relation `makes processes further than'.
Thus, we obtain the first spectrum of behavioral metrics on the PTS model.
From this spectrum we derive an analogous one for the kernels of the metrics, ordered by the relation `makes strictly less identification than'.
Finally, we introduce a novel technique for the logical characterization of both behavioral metrics and their kernels, based on the notions of mimicking formula and distance on formulae.
This kind of characterization allows us to obtain the first example of a spectrum of distances on processes obtained directly from logics.
Moreover, we show that the kernels of the metrics can be characterized by simply comparing the mimicking formulae of processes
Back to the format: A survey on SOS for probabilistic processes
Full text linkIn probabilistic process algebras the classic qualitative description of process behaviour is enriched with quantitative information on it, usually modelled in terms of probabilistic weights and/or distributions over the qualitative behaviour. In this setting, we use behavioural equivalences to check whether two processes show exactly the same behaviour, and, if this is not the case, we can use behavioural metrics to measure the distance between them. Compositional reasoning requires that equivalence, or closeness, of behaviour of two processes are not destroyed when language operators are applied on top of them in order to build larger processes. Formally, the equivalence must be a congruence, and the metric must be uniformly continuous, with respect to language operators. Instead of verifying these compositional properties by hand, operator-by-operator, it is much more convenient to prove them for a class of operators once for all, and to check that the operators one is dealing with are in that class. This is achieved by means of SOS specification formats: they consist in a set of syntactical constraints characterising a class of operators on the patterns of SOS rules, that define the operational semantics of languages. With this survey, we aim to collect and describe the specification formats that have been proposed in the literature to guarantee the compositional properties of (variants of) bisimulation equivalences and bisimulation metrics in the probabilistic setting.</p
Logical Characterization of Trace Metrics
No full textIn this paper we continue our research line on logical characterizations of behavioralmetrics obtained from the definition of a metric over the set of logical properties of interest. This time we provide a characterization of both strong and weak trace metric on nondeterministic probabilistic processes, based on a minimal boolean logic L which we prove to be powerful enough to characterize strong and weak probabilistic trace equivalence. Moreover,we also prove that our characterization approach can be restated in terms of a more classic probabilistic L-model checking problem
Robustness for biochemical networks:Step-by-step approach
Full text linkWe propose two step-by-step approaches to the analysis of robustness in biochemical networks. Our aim is to measure the ability of the network to exhibit step-by-step limited variations on the concentration of a species of interest at varying of the initial concentration of other species. The first approach we propose is reaction-by-reaction, i.e. we compare the states reached by nominal and perturbed networks after they have performed the same number of reactions. We provide a statistical technique allowing for estimating robustness, we implement it in a tool called SPEBNR (a Simple Python Environment for statistical estimation of Biochemical Network Robustness) and showcase it on three case studies: the EnvZ/OmpR osmoregulatory signaling system of Escherichia Coli, the mechanism of bacterial chemotaxis of Escherichia Coli, and enzyme activity at saturation. Then, we consider a time-by-time approach, in which networks are compared on the basis of the states they reached at the same time point, regardless of how many reactions occurred. This approach is implemented in STARK, and we apply it to the study the robustness of the EnvZ/OmpR osmoregulatory signaling system and the Lotka-Volterra equations.</p
Modal Decomposition on Nondeterministic Probabilistic Processes
Full text linkWe propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes.
The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition.
By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity
DT-Stark: a tool for evaluating the effectiveness of digital twins through feedback and perturbations
No full textA digital twin is a virtual replica of a physical system that has to interact with it in real-time in order to facilitate decision-making, to reduce failures and costs, and to ensure a coherent and safe system execution. We call effectiveness the ability of the digital twin to direct the physical counterpart. In this paper we provide the means to evaluate the effectiveness of a digital twin in the case that the physical system is operating under uncertainty, and it is therefore subject to perturbations. Specifically, we present the DT-Stark tool, that extends Stark, a tool for modelling and verification of systems operating under uncertainty, with feedback, a special mechanism that allow us to model the communications, and their effects, between the digital and the physical (perturbed) twin in a concise, clean fashion. We can then exploit the features of Stark to compare the behaviour of the twins, to verify properties over them, and to measure effectiveness. We provide some examples of the use of our tool by applying it to the evaluation of the effectiveness of digital twins in two robotic scenarios: an industrial plant and a smart hospital
RobTL: Robustness Temporal Logic for CPS
Full text linkWe propose Robustness Temporal Logic (RobTL), a novel temporal logic for the specification and analysis of distances between the behaviours of Cyber-Physical Systems (CPS) over a finite time horizon. RobTL specifications allow us to measure the differences in the behaviours of systems with respect to various objectives and temporal constraints, and to study how those differences evolve in time. Specifically, the unique features of RobTL allow us to specify robustness properties of CPS against uncertainty and perturbations. As an example, we use RobTL to analyse the robustness of an engine system that is subject to attacks aimed at inflicting overstress of equipment
- …
