An Experimental Toolchain for Strategy Synthesis with Spatial Properties

被引：6

作者：

Basile, Davide ^{[1
]}

ter Beek, Maurice H. ^{[1
]}

Ciancia, Vincenzo ^{[1
]}

机构：

[1] ISTI CNR, Formal Methods & Tools Lab, Pisa, Italy

来源：

LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION. ADAPTATION AND LEARNING, ISOLA 2022, PT III | 2022年 / 13703卷

关键词：

SUPERVISORY CONTROL; SYSTEM;

D O I：

10.1007/978-3-031-19759-8_10

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker that allows the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. In this paper, we explore the integration of these two tools. We provide a basic example of strategy synthesis on automata encoding motion of agents in spaces represented by images. The strategy is synthesised with CATLib, whilst the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA.

引用

页码：142 / 164

页数：23

共 65 条

[1] Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications [J].

Alsalehi, Suhail ;

Mehdipour, Noushin ;

Bartocci, Ezio ;

Belta, Calin .

2021 60TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2021, :5110-5115

[2] Compositional Synthesis of Reactive Controllers for Multi-agent Systems [J].

Alur, Rajeev ;

Moarref, Salar ;

Topcu, Ufuk .

COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 9780 :251-269

[3]

Asarin E, 1998, SYSTEM STRUCTURE AND CONTROL 1998 (SSC'98), VOLS 1 AND 2, P447

[4] Relating two automata-based models of orchestration and choreography [J].

Basile, D. ;

Degano, P. ;

Ferrari, G. L. ;

Tuosto, E. .

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2016, 85 (03) :425-446

[5]

Basile D., Repository for reproducing the experiments

[6]

Basile D., 2017, P 11 INT WORKSH VAR, P20, DOI DOI 10.1145/3023956.3023965

[7]

Basile D, 2023, Arxiv, DOI [arXiv:2203.14122, 10.48550/arXiv.2203.14122, DOI 10.48550/ARXIV.2203.14122]

[8] A Clean and Efficient Implementation of Choreography Synthesis for Behavioural Contracts [J].

Basile, Davide ;

ter Beek, Maurice H. .

COORDINATION MODELS AND LANGUAGES, COORDINATION 2021, 2021, 12717 :225-238

[9] Contract Automata Library [J].

Basile, Davide ;

ter Beek, Maurice H. .

SCIENCE OF COMPUTER PROGRAMMING, 2022, 221

[10] Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with UPPAAL STRATEGO [J].

Basile, Davide ;

ter Beek, Maurice H. ;

Legay, Axel .

FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2020, 2020, 12136 :3-21

← 1 2 3 4 5 6 7 →