Search Results

Documents authored by Castiglioni, Valentina

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.CONCUR.2022.6
On the Axiomatisation of Branching Bisimulation Congruence over CCS

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2022.6,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{On the Axiomatisation of Branching Bisimulation Congruence over CCS}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.6},
  URN =		{urn:nbn:de:0030-drops-170692},
  doi =		{10.4230/LIPIcs.CONCUR.2022.6},
  annote =	{Keywords: Equational basis, Weak semantics, CCS, Parallel composition}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.8
Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

Authors: Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.
Cite as

Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2021.8,
  author =	{Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.8},
  URN =		{urn:nbn:de:0030-drops-134425},
  doi =		{10.4230/LIPIcs.CSL.2021.8},
  annote =	{Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.18
On the Axiomatisability of Parallel Composition: A Journey in the Spectrum

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen. On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.18,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas and Pedersen, Mathias Ruggaard},
  title =	{{On the Axiomatisability of Parallel Composition: A Journey in the Spectrum}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.18},
  URN =		{urn:nbn:de:0030-drops-128303},
  doi =		{10.4230/LIPIcs.CONCUR.2020.18},
  annote =	{Keywords: Axiomatisation, Parallel composition, Linear time-branching time spectrum}
}
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}
}
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