2026

J. Xiang, R. Lanotte, S. Tini,  M. Merro: 

Formal Quantitative Tolerance of Cyber-Physical Systems Under Periodic Attacks.

IEEE Access 14


J. De Jong, V. Castiglioni, S. Tini:

Robustness Against Timed Distorsion in STARK.

FORTE 2026


2025


J. Xiang, R. Lanotte, S. Tini,  M. Merro:

Formal Robustness for Cyber-Physical Systems under Timed Attacks

CSF 2025, IEEE.


J. Xiang, R. Lanotte, S. Tini, S. Chong, M. Merro:

Measuring Robustness in Cyber-Physical Systems under Sensor Attacks

Nonlinear Analysis: Hybrid Systems, 56, 101559 (2025).


V. Castiglioni, R. Lanotte, M. Loreti, S. Tini:

DT-STARK: A Tool for Evaluating the Effectiveness of Digitsl Twins throuhg Feedback and Perturbations.

Int. J. Softw. toold Technol. Transf. 25(5): 443-464.


2024


V. Castiglioni,  R. Lanotte, M. Loreti, D. Manicardi, S. Tini:

Robustness for biochemical networks: Step-by-step approach

Theoretical Computer Science,  1022, 114934 (2024).


V. Castiglioni, M. Loreti, S. Tini:

RobTL: Robustness Temporal Logic for CPS

CONCUR 2024. LIPIcs 311, 2024, 15.


V. Castiglioni, M. Loreti, S. Tini:

STARK: A tool for the analysis of CPSs robustness

Science of Computer Programming 236: 103134 (2024).


V. Castiglioni, M. Loreti, S. Tini:

Bio-Stark: A Tool for the Time-Point Robustness Analysis of Biological Systems

CMSB 2024, LNCS 14971.


V. Castiglioni, R. Lanotte, M. Loreti, S. Tini:

Evaluating the Effectiveness of Digital Twins Through Statistical Model Checking with Feedback and Perturbations

FMICS 2024,  LNCS 14952.


V. Castiglioni, R. Lanotte, S. Tini:

Back to the format: A survey on SOS for probabilistic processes

Journal of Logical and Algebraic Methods in Programming 137:100929 (2024).


2023


S. Manicardi, R. Lanotte, S. Tini:

Step-by-step Robustness for Biochemical Networks

ICTCS 2023, CEUR, 299-313.


V. Castiglioni, M. Loreti, S. Tini:

DisTL: A Temporal Logic for the Analysis of the Expected Behaviour of Cyber-Physical Systems

ICTCS 2023, CEUR, 15-30.


S. Chong, R. Lanotte, M. Merro, S. Tini, J. Xiang:

Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems

HSCC 2023, ACM.


V. Castiglioni, M. Loreti, S. Tini:

A framework to measure the robustness of programs in the unpredictable environment

Logical Methods in Computer Science 19(3), 2:1-2:46 (2023)


V. Castiglioni, M. Loreti, S. Tini:

STARK: A Software Tool for the Analysis of Robustness in the unKnown environment

COORDINATION 2023, LNCS.


2021


R. Lanotte, M. Merro, A. Monteanu, S. Tini:

Formal Impact Metrics for Cyber-Physical Systems

CSF 2021, IEEE.


V. Castiglioni, M. Loreti, S. Tini:

How Adaptable and Reliable is your System?

FORTE 2021, LNCS 12719, 60-79.


R. Lanotte, S. Tini:

A Weak Semantic Approach to Bisimulation Metrics in Models with Nondeterminism and Continuous State Spaces

Theoretical Computer Science 869 (2021) 29-61.


R. Lanotte, M. Merro, S. Tini:

A Probabilistic Calculus of Cyber-Physical Systems

Information and Computation 279:104618 (2021).


2020


V. Castiglioni, M. Loreti, S. Tini:

Measuring Adaptability and Reliability of Large Scale Systems

ISoLA 2020, LNCS 12477, 380-396.


V. Castiglioni, S. Tini:

Raiders of the lost equivalence: Probabilistic branching bisimilarity

Information Processing Letters 159-160 (2020)


V. Castiglioni, M. Loreti, S. Tini:

The Metric Linear Time-Branching Time Spetrum on Nondeterministic Probabilistic Processes

Theoretical Computer Science 813 (2020) 20-69.


A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, F. Schiavio, S. Tini:

CospanSpan(Graph): a Compositional Description of the Heart System

Fundamenta Informaticae 171 (2020) 221-237


V. Castiglioni, S. Tini:

Probabilistic Divide & Congruence: Branching Bisimilarity

Theoretical Computer Science 808, 147-196 (2020).


2019


R. Lanotte, S. Tini:

Computing Bisimilarity Metrics for Probabilistic Timed Automata

iFM 2019, LNCS 11918, 303-321.


R. Lanotte, S. Tini:

Fully syntactic uniform continuity formats for bisimulation metrics.

The Art of Modelling Computational Systems, LNCS 11760, 2019, 293-312.


V. Castiglioni, S. Tini:

Logical Characterization of Branching Metrics for Nondeterministic Probabilistic Transition Systems

Information and Computation 268 (2019).


2018


R. Lanotte, M. Merro, S. Tini:

Equational reasoning in wireless network gossip protocols

Logical Methods in computer Science 14(3) (2018).


R. Lanotte, S. Tini:

Weak bisimulation metrics in models with nondeterminism and continuous state spaces

ICTAC 2018, LNCS 11187, 292-312.


R. Lanotte, M. Merro, S. Tini:

Towards a formal notion of impact metric for cyber-physical attacks

iFM 2018, LNCS 11023, 296-315.


V. Castiglioni, D. Gebler, S. Tini:

SOS modal decomposition on nondeterministic probabilistic processes

Logical Methods in Computer Science 14(2) (2018).


D. Gebler, S. Tini:

SOS specifications for uniformly continuous operators

Journal of Computer and System Sciences 92: 113-151 (2018).


2017


R. Lanotte, M. Merro, S. Tini:

Weak Simulation Quasimetric in a Gossip Scenario

FORTE 2017, LNCS 10321, 139-155.


R. Lanotte, M. Merro, S. Tini:

Compositional Weak Metrics for Group Key Update

MFCS 2017, LIPICS, 72:1-72:14.


V. Castiglioni, S. Tini:

Logical Characterizaion of Trace Metric

QAPL 2017, EPTCS.


2016


D. Gebler, Kim G. Larsen, S. Tini:

Compositional bisimulation metric reasoning with Probabilistic Process Calculi

Logical Methods in Computer Science 12(4) (2016).


V. Castiglioni, R. Lanotte, S. Tini:

A Function Elimination Method for Checking Satisfiability of Arithmetical Logics

Fundamenta Informatica 143(1-2): 51-71 (2016).


V. Castiglioni, D. Gebler, S. Tini:

Modal Decomposition on Nondeterministic Probabilistic Processes

CONCUR 2016, LIPIcs 59, 36:1-36:15.


R. Lanotte, S. Tini:

Extending Taylor Approximation to Hybrid Systems with Integrals

CS&P 2016, 141-152.


V. Castiglioni, D. Gebler, S. Tini:

Logical Characterizaion of Bisimulation Metric

QAPL 2016, EPTCS 227, 44-62.


2015


D. Gebler, S. Tini:

SOS specifications of probabilistic systems by uniformly continuous operators

CONCUR 2015, LIPIcs 42, 155-168.


D. Gebler, K.G. Larsen, S. Tini:

Compositional metric reasoning with probabilistic process calculi

FoSSaCS 2015, LNCS 9034, 230-245.


2014


V. Castiglioni, R. Lanotte, S. Tini:

A specification format for rooted branching bisimulation

Fundamenta Informaticae 135(4): 355-369 (2014).


G. Pardini, R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

Compositional semantics and behavioural equivalences for reaction systems with restriction

Theoretical Computer Science 551: 1-21 (2014).


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, G. Pardini, S. Tini:

Systolic Automata and P Systems

Computing with New Resources, LNCS 8808, 2014: 17-31.


D. Gebler, S. Tini:

Fixed-point characterization of compositionality properties of probabilistic processes combinators

EXPRESS/SOS 2014, EPTCS 160, 63-78.


2013


G. Pardini, R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

A compositional semantics of Reaction Systems with restriction

CiE 2013, LNCS 7921, 330-339.


D. Gebler, S. Tini:

Compositionality of approximate bisimulation for probabilistic systems

EXPRESS/SOS 2013, EPTCS 120, 32-46.


2012


R. Barbuti, G. Caravagna, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

Foundationals aspects of multiscale modelling of biological systems with process algebras

Theoretical Computer Science 431: 96-116 (2012).


2011


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

An overview on operational semantics in membrane computing

International Journal of Foundations of Computer Science 22(1): 119-131 (2011).


2010


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

Compositional semantics of spiking neural P systems

The Journal of Logic and Algebraic Programming 79(6): 304-316 (2010).


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

Membrane systems working in generating and accepting modes: Expressiveness and encodings

Membrane Computing 2010, LNCS 6501: 103-118.


S. Tini:

Non-expansive epsilon-bisimulations for probabilistic processes

Theoretical Computer Science 411(22-24): 2202-2222 (2010).


R. Barbuti, G. Caravagna, P. Milazzo, A. Maggiolo-Schettini, S. Tini:

Aspects of multiscale modelling in a process algebra for biological systems

MeCBIC 2010, EPTCS 40, 54-69.


2009


R. Lanotte, S. Tini:

Probabilistic bisimulation as a congruence

ACM Transactions on Computational Logic 10(2): (2009).


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

P Systems with Transport and Diffusion Membrane Channels

Fundamenta Informaticae 93(1-3): 17-31 (2009).


2008


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

A P systems flat form preserving step-by-step behaviour

Fundamenta Informaticae 87(1): 1-34 (2008).


R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, S. Tini:

Compositional semantics and behavioral equivalences for P Systems

Theoretical Computer Science 395(1): 77-100 (2008).


S. Tini:

Non expansive epsilon-Bisimulations

AMAST 2008, LNCS, 362-376.


2007


R. Lanotte, S. Tini:

Taylor approximation for hybrid systems

Information and Computation 205(11): 1575-1607 (2007).


2006


S. Tini:

Notes on generative probabilistic bisimulation

SOS 2006, ENTCS 175(1), 77-88.


2005


R. Lanotte, S. Tini:

Probabilistic congruence for semistochastic generative processes

FoSSaCS 2005, LNCS 3441, 63-78.


R. Lanotte, S. Tini:

Taylor approximation for hybrid systems

HSCC 2005, LNCS 3414, 402-416.


2004


R. Lanotte, A. Maggiolo-Schettini, S. Tini, A. Troina, E. Tronci:

Automatic covert channel analysis of a multilevel secure component

ICICS 2004, LNCS 3269, 249-261.


R. Lanotte, A. Maggiolo-Schettini, S. Tini:

Information flow in hybrid systems

ACM Transactions on Embedded Computer Systems 3(4): 760-799 (2004).


R. Lanotte, A. Maggiolo-Schettini, S. Tini, A. Troina, E. Tronci:

Automatic analysis of the NRL Pump

ENTCS 99, 2004, 245-266.


S. Tini:

Timed CCP compositionally embeds Argos and Lustre

Formal Aspects of Computing 16(3): 292-312 (2004).


S. Tini, A. Maggiolo-Schettini:

Compositional synthesis of generalized Mealy machines

Fundamenta Informaticae 60(1-4): 367-382 (2004).


R. Lanotte, A Maggiolo-Schettini, S. Tini:

Epsilon-transitions in concurrent timed automata

Information Processing Letters 89(1): 1-7 (2004)


R. Gorrieri, R. Lanotte, A. Maggiolo-Schettini, F. Martinelli, S. Tini, E. Tronci:

Automated analysis of timed security: a case study on web privacy

International Journal of Information Security 2(3-4): 168-186 (2004).


S. Tini:

Rule formats for compositional non-interference properties

The Journal of Logic and Algebraic Programming 60-61: 353-400 (2004).


2003


S. Tini:

Rule Formats for Non Interference

ESOP 2003, LNCS 2618, 129-143.


R. Lanotte, A. Maggiolo-Schettini, A. Peron, S. Tini:

Dynamic Hierarchical Machines

Fundamenta Informaticae 54(2-3): 237-252 (2003).


S. Tini:

An axiomatic semantics for the synchronous language Gentzen

Journal of Computer and System Sciences 66(2): 316-348 (2003).


A. Maggiolo-Schettini, A. Peron, S. Tini:

A comparison of Statecharts step semantics

Theoretical Computer Science 290(1): 465-498 (2003).


R. Lanotte, A. Maggiolo-Schettini, S. Tini:

Concurrency in timed automata

Theoretical Computer Science 309(1-3): 503-527 (2003).


2002


A. Maggiolo-Schettini, S. Tini:

On disjunction of literals in triggers of Statecharts transitions

Information Processing Letters 84(6): 305-310 (2002).


2001


R. Lanotte, A. Maggiolo-Schettini, S. Tini:

Privacy in Real-Time Systems

MTCS 2001, ENTCS 52(3), 295-305.


R. Focardi, R. Gorrieri, R. Lanotte, A. Maggiolo-Schettini, F. Martinelli, S. Tini, E. Tronci:

Formal models of timing attacks on web privacy

ENTCS 62, 2001, 229-243.


R. Lanotte, A. Maggiolo-Schettini, S. Tini, A. Peron:

Transformations of timed cooperating automata

Fundamenta Informaticae 47(3-4): 271-282 (2001).


S. Tini:

An axiomatic semantics for Esterel

Theoretical Computer Science 269(1-2): 231-282 (2001).


R. Lanotte, A. Maggiolo-Schettini, S.Tini:

Concurrency in timed automata

FCT 2001, LNCS 2138, 240-251.


S. Tini:

An Axiomatic Semantics for the synchronous language Gentzen

FoSSaCS 2001, LNCS 2030, 394-409.


2000


S. Tini, A. Maggiolo-Schettini:

A causal semantics for Timed Default Concurrent Constraint Programming

AMAST 2000, LNCS 1816, 228-242.


1999


A. Maggiolo-Schettini, S. Tini:

Applying techniques of asynchronous concurrency to synchronous languages

Fundamenta Informaticae 40(2-3): 221-250 (1999).


S. Tini:

On the expressiveness of Timed Concurrent Constraint Programming

EXPRESS 1999, ENTCS 27, 3-17.


S. Tini, Andrea Maggiolo-Schettini:

A truly concurrent semantics for Timed Default Concurrent Constraint Programming

ECOOP Workshops 1999, LNCS 1743, 256-257.


1998


S. Tini, A. Maggiolo-Schettini:

Two semantics for Timed Default Concurrent Constraint Programming

COTIC 1998, ENTCS 16(1), 24-41.


A. Maggiolo-Schettini, S. Tini:

Projectable Semantics for Statecharts

MFCS 98 Workshop on Concurrency, ENTCS 18, 134-146.


1996


A. Maggiolo-Schettini, A. Peron, S. Tini:

Equivalences of Statecharts

CONCUR 1996, LNCS 1119, 687-702.