Document - An experimental toolchain for strategy synthesis with spatial properties

2022

Conference article Open Access

An experimental toolchain for strategy synthesis with spatial properties

Basile D., Ter Beek M. H., Ciancia V.

Synthesis Games Spatial model checking Multi-agent systems Rigorous tool engineering

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.

Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:471909,
	title = {An experimental toolchain for strategy synthesis with spatial properties},
	author = {Basile D. and Ter Beek M. H. and Ciancia V.},
	doi = {10.1007/978-3-031-19759-8_10},
	booktitle = {ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022},
	year = {2022}
}