Source author record

Simone Tini

Simone Tini appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Computational Engineering, Finance, and Science Formal Languages and Automata Theory Programming Languages

Catalog footprint

What is connected

5works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

EvTL: A Temporal Logic for the Transient Analysis of Cyber-Physical Systems

The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to perturbations and uncertainties. In this paper we propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Evolution Temporal Logic (EvTL), a stochastic extension of STL allowing us to specify properties of the probability distributions describing the transient behaviour of systems, and to include the presence of uncertainties in the specification. We equip EvTL with a robustness semantics and we prove it sound and complete with respect to the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we develop a statistical model checking algorithm for EvTL specifications. As an example of an application of our framework, we consider a three-tanks laboratory experiment.

preprint2016arXiv

Logical Characterization of Bisimulation Metrics

Bisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on the novel notions of mimicking formulae and distance between formulae. The former are a weak version of the well known characteristic formulae and allow us to characterize also (ready) probabilistic simulation and probabilistic bisimilarity. The latter is a 1-bounded pseudometric on formulae that mirrors the Hausdorff and Kantorovich lifting the defining bisimilarity pseudometric. We show that the distance between two processes equals the distance between their own mimicking formulae.

preprint2014arXiv

Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators

Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes.

preprint2013arXiv

Compositionality of Approximate Bisimulation for Probabilistic Systems

Probabilistic transition system specifications using the rule format ntmuft-ntmuxt provide structural operational semantics for Segala-type systems and guarantee that probabilistic bisimilarity is a congruence. Probabilistic bisimilarity is for many applications too sensitive to the exact probabilities of transitions. Approximate bisimulation provides a robust semantics that is stable with respect to implementation and measurement errors of probabilistic behavior. We provide a general method to quantify how much a process combinator expands the approximate bisimulation distance. As a direct application we derive an appropriate rule format that guarantees compositionality with respect to approximate bisimilarity. Moreover, we describe how specification formats for non-standard compositionality requirements may be derived.

preprint2010arXiv

Aspects of multiscale modelling in a process algebra for biological systems

We propose a variant of the CCS process algebra with new features aiming at allowing multiscale modelling of biological systems. In the usual semantics of process algebras for modelling biological systems actions are instantaneous. When different scale levels of biological systems are considered in a single model, one should take into account that actions at a level may take much more time than actions at a lower level. Moreover, it might happen that while a component is involved in one long lasting high level action, it is involved also in several faster lower level actions. Hence, we propose a process algebra with operations and with a semantics aimed at dealing with these aspects of multiscale modelling. We study behavioural equivalences for such an algebra and give some examples.