On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK

Sebastián Betancourt; Valentina Castiglioni

doi:10.1007/978-3-031-94533-5_16

On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK

Sebastián Betancourt (Corresponding author)
, Valentina Castiglioni

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

9 Downloads (Pure)

Abstract

Stark has been introduced for the specification, analysis and verification of cyber-physical systems operating under uncertainty. In this paper, we apply it to the modelling and safety analysis of several instances of a highway environment with autonomous vehicles: One vehicle will be controlled by a Stark agent, while the others are modelled as part of a Stark environment. Given the unpredictable behaviour of the environment, we analyse some safety guarantees on the behaviour of the agent in terms of its robustness against perturbations by means of the temporal logic RobTL and statistical model checking. We then discuss the use of Stark for the validation of the behaviour of reinforcement learning agents in the highway environment with the temporal logic DisTL.

Original language	English
Title of host publication	Rigorous State-Based Methods
Subtitle of host publication	11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings
Editors	Michael Leuschel, Fuyuki Ishikawa
Place of Publication	Cham
Publisher	Springer
Pages	269-287
Number of pages	19
ISBN (Electronic)	978-3-031-94533-5
ISBN (Print)	978-3-031-94532-8
DOIs	https://doi.org/10.1007/978-3-031-94533-5_16
Publication status	Published - 2 Jun 2025
Event	11th International Rigorous State-Based Methods, ABZ 2025 - Düsseldorf, Germany Duration: 10 Jun 2025 → 13 Jun 2025

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	15728
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Rigorous State-Based Methods, ABZ 2025
Abbreviated title	ABZ 2025
Country/Territory	Germany
City	Düsseldorf
Period	10/06/25 → 13/06/25

Access to Document

10.1007/978-3-031-94533-5_16

pdfFinal published version, 3.25 MBLicence: TAVERNE

Cite this

Betancourt, S., & Castiglioni, V. (2025). On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK. In M. Leuschel, & F. Ishikawa (Eds.), Rigorous State-Based Methods: 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings (pp. 269-287). (Lecture Notes in Computer Science (LNCS); Vol. 15728). Springer. https://doi.org/10.1007/978-3-031-94533-5_16

Betancourt, Sebastián ; Castiglioni, Valentina. / On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK. Rigorous State-Based Methods: 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings. editor / Michael Leuschel ; Fuyuki Ishikawa. Cham : Springer, 2025. pp. 269-287 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{e5abe783b3ba41dcb49f73b38c70f4a0,

title = "On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK",

abstract = "Stark has been introduced for the specification, analysis and verification of cyber-physical systems operating under uncertainty. In this paper, we apply it to the modelling and safety analysis of several instances of a highway environment with autonomous vehicles: One vehicle will be controlled by a Stark agent, while the others are modelled as part of a Stark environment. Given the unpredictable behaviour of the environment, we analyse some safety guarantees on the behaviour of the agent in terms of its robustness against perturbations by means of the temporal logic RobTL and statistical model checking. We then discuss the use of Stark for the validation of the behaviour of reinforcement learning agents in the highway environment with the temporal logic DisTL.",

author = "Sebasti{\'a}n Betancourt and Valentina Castiglioni",

year = "2025",

month = jun,

day = "2",

doi = "10.1007/978-3-031-94533-5\_16",

language = "English",

isbn = "978-3-031-94532-8",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "269--287",

editor = "Michael Leuschel and Fuyuki Ishikawa",

booktitle = "Rigorous State-Based Methods",

address = "Germany",

note = "11th International Rigorous State-Based Methods, ABZ 2025, ABZ 2025 ; Conference date: 10-06-2025 Through 13-06-2025",

}

Betancourt, S & Castiglioni, V 2025, On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK. in M Leuschel & F Ishikawa (eds), Rigorous State-Based Methods: 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings. Lecture Notes in Computer Science (LNCS), vol. 15728, Springer, Cham, pp. 269-287, 11th International Rigorous State-Based Methods, ABZ 2025, Düsseldorf, Germany, 10/06/25. https://doi.org/10.1007/978-3-031-94533-5_16

On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK. / Betancourt, Sebastián (Corresponding author); Castiglioni, Valentina.
Rigorous State-Based Methods: 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings. ed. / Michael Leuschel; Fuyuki Ishikawa. Cham: Springer, 2025. p. 269-287 (Lecture Notes in Computer Science (LNCS); Vol. 15728).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK

AU - Betancourt, Sebastián

AU - Castiglioni, Valentina

PY - 2025/6/2

Y1 - 2025/6/2

N2 - Stark has been introduced for the specification, analysis and verification of cyber-physical systems operating under uncertainty. In this paper, we apply it to the modelling and safety analysis of several instances of a highway environment with autonomous vehicles: One vehicle will be controlled by a Stark agent, while the others are modelled as part of a Stark environment. Given the unpredictable behaviour of the environment, we analyse some safety guarantees on the behaviour of the agent in terms of its robustness against perturbations by means of the temporal logic RobTL and statistical model checking. We then discuss the use of Stark for the validation of the behaviour of reinforcement learning agents in the highway environment with the temporal logic DisTL.

AB - Stark has been introduced for the specification, analysis and verification of cyber-physical systems operating under uncertainty. In this paper, we apply it to the modelling and safety analysis of several instances of a highway environment with autonomous vehicles: One vehicle will be controlled by a Stark agent, while the others are modelled as part of a Stark environment. Given the unpredictable behaviour of the environment, we analyse some safety guarantees on the behaviour of the agent in terms of its robustness against perturbations by means of the temporal logic RobTL and statistical model checking. We then discuss the use of Stark for the validation of the behaviour of reinforcement learning agents in the highway environment with the temporal logic DisTL.

U2 - 10.1007/978-3-031-94533-5_16

DO - 10.1007/978-3-031-94533-5_16

M3 - Conference contribution

SN - 978-3-031-94532-8

T3 - Lecture Notes in Computer Science (LNCS)

SP - 269

EP - 287

BT - Rigorous State-Based Methods

A2 - Leuschel, Michael

A2 - Ishikawa, Fuyuki

PB - Springer

CY - Cham

T2 - 11th International Rigorous State-Based Methods, ABZ 2025

Y2 - 10 June 2025 through 13 June 2025

ER -

Betancourt S , Castiglioni V. On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK. In Leuschel M, Ishikawa F, editors, Rigorous State-Based Methods: 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings. Cham: Springer. 2025. p. 269-287. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-031-94533-5_16

On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with STARK

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this