Search Results

Documents authored by Tini, Simone

Artifact
Software
DOI: 10.4230/artifacts.22451
STARK: A Software Tool for the Analysis of Robustness in the unKnown environment

Authors: Valentina Castiglioni, Michele Loreti, and Simone Tini

Abstract
Cite as

Valentina Castiglioni, Michele Loreti, Simone Tini. STARK: A Software Tool for the Analysis of Robustness in the unKnown environment (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22451,
   title = {{STARK: A Software Tool for the Analysis of Robustness in the unKnown environment}}, 
   author = {Castiglioni, Valentina and Loreti, Michele and Tini, Simone},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:ddfb418d5a080b8e83323a1b2c38d9f7065e2554;origin=https://github.com/quasylab/jspear;visit=swh:1:snp:8132c5d3ed79097d14de6b333de38b74741c7f2f;anchor=swh:1:rev:c6b2386d36b72ab790999d2963203b7d5aa03ce7}{\texttt{swh:1:dir:ddfb418d5a080b8e83323a1b2c38d9f7065e2554}} (visited on 2024-11-28)},
   url = {https://github.com/quasylab/jspear/tree/working},
   doi = {10.4230/artifacts.22451},
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.15
RobTL: Robustness Temporal Logic for CPS

Authors: Valentina Castiglioni, Michele Loreti, and Simone Tini

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We 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.
Cite as

Valentina Castiglioni, Michele Loreti, and Simone Tini. RobTL: Robustness Temporal Logic for CPS. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{castiglioni_et_al:LIPIcs.CONCUR.2024.15,
  author =	{Castiglioni, Valentina and Loreti, Michele and Tini, Simone},
  title =	{{RobTL: Robustness Temporal Logic for CPS}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{15:1--15:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.15},
  URN =		{urn:nbn:de:0030-drops-207870},
  doi =		{10.4230/LIPIcs.CONCUR.2024.15},
  annote =	{Keywords: Cyber-physical systems, robustness, temporal logic, uncertainty}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.72
Compositional Weak Metrics for Group Key Update

Authors: Ruggero Lanotte, Massimo Merro, and Simone Tini

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We investigate the compositionality of both weak bisimilarity metric and weak similarity quasi- metric semantics with respect to a variety of standard operators, in the context of probabilistic process algebra. We show how compositionality with respect to nondeterministic and probabilistic choice requires to resort to rooted semantics. As a main application, we demonstrate how our results can be successfully used to conduct compositional reasonings to estimate the performances of group key update protocols in a multicast setting.
Cite as

Ruggero Lanotte, Massimo Merro, and Simone Tini. Compositional Weak Metrics for Group Key Update. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{lanotte_et_al:LIPIcs.MFCS.2017.72,
  author =	{Lanotte, Ruggero and Merro, Massimo and Tini, Simone},
  title =	{{Compositional Weak Metrics for Group Key Update}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{72:1--72:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.72},
  URN =		{urn:nbn:de:0030-drops-81262},
  doi =		{10.4230/LIPIcs.MFCS.2017.72},
  annote =	{Keywords: Behavioural metric, compositional reasoning, group key update}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.36
Modal Decomposition on Nondeterministic Probabilistic Processes

Authors: Valentina Castiglioni, Daniel Gebler, and Simone Tini

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We 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.
Cite as

Valentina Castiglioni, Daniel Gebler, and Simone Tini. Modal Decomposition on Nondeterministic Probabilistic Processes. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{castiglioni_et_al:LIPIcs.CONCUR.2016.36,
  author =	{Castiglioni, Valentina and Gebler, Daniel and Tini, Simone},
  title =	{{Modal Decomposition on Nondeterministic Probabilistic Processes}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.36},
  URN =		{urn:nbn:de:0030-drops-61665},
  doi =		{10.4230/LIPIcs.CONCUR.2016.36},
  annote =	{Keywords: SOS, nondeterministic probabilistic process algebras, logical characterization, decomposition of modal formulae}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.155
SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators

Authors: Daniel Gebler and Simone Tini

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Compositional reasoning over probabilistic systems wrt. behavioral metric semantics requires the language operators to be uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows us to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators.
Cite as

Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 155-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gebler_et_al:LIPIcs.CONCUR.2015.155,
  author =	{Gebler, Daniel and Tini, Simone},
  title =	{{SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{155--168},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.155},
  URN =		{urn:nbn:de:0030-drops-53876},
  doi =		{10.4230/LIPIcs.CONCUR.2015.155},
  annote =	{Keywords: SOS, probabilistic process algebra, bisimulation metric semantics, compositional metric reasoning, uniform continuity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact