View in EDS

A toolchain for strategy synthesis with spatial properties.

Saved in:
Bibliographic Details
Title: A toolchain for strategy synthesis with spatial properties.
Authors: Basile, Davide1 (AUTHOR) davide.basile@isti.cnr.it, ter Beek, Maurice H.1 (AUTHOR), Bussi, Laura1 (AUTHOR), Ciancia, Vincenzo1 (AUTHOR)
Source: International Journal on Software Tools for Technology Transfer. Dec2023, Vol. 25 Issue 5/6, p641-658. 18p.
Subjects: Multiagent systems, Pixels, Strategy games, Finite state machines, Digital images, Digital technology, Proof of concept
Abstract: We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools CATLib and VoxLogicA to interact in a fully automated way. The Contract Automata Library (CATLib) is aimed at 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 for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with CATLib, while the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements. [ABSTRACT FROM AUTHOR]
Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 173850959
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A toolchain for strategy synthesis with spatial properties.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Basile%2C+Davide%22">Basile, Davide</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> davide.basile@isti.cnr.it</i><br /><searchLink fieldCode="AR" term="%22ter+Beek%2C+Maurice+H%2E%22">ter Beek, Maurice H.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Bussi%2C+Laura%22">Bussi, Laura</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Ciancia%2C+Vincenzo%22">Ciancia, Vincenzo</searchLink><relatesTo>1</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22International+Journal+on+Software+Tools+for+Technology+Transfer%22">International Journal on Software Tools for Technology Transfer</searchLink>. Dec2023, Vol. 25 Issue 5/6, p641-658. 18p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Multiagent+systems%22">Multiagent systems</searchLink><br /><searchLink fieldCode="DE" term="%22Pixels%22">Pixels</searchLink><br /><searchLink fieldCode="DE" term="%22Strategy+games%22">Strategy games</searchLink><br /><searchLink fieldCode="DE" term="%22Finite+state+machines%22">Finite state machines</searchLink><br /><searchLink fieldCode="DE" term="%22Digital+images%22">Digital images</searchLink><br /><searchLink fieldCode="DE" term="%22Digital+technology%22">Digital technology</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+of+concept%22">Proof of concept</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools CATLib and VoxLogicA to interact in a fully automated way. The Contract Automata Library (CATLib) is aimed at 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 for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with CATLib, while the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=173850959
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10009-023-00730-1
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 18
        StartPage: 641
    Subjects:
      – SubjectFull: Multiagent systems
        Type: general
      – SubjectFull: Pixels
        Type: general
      – SubjectFull: Strategy games
        Type: general
      – SubjectFull: Finite state machines
        Type: general
      – SubjectFull: Digital images
        Type: general
      – SubjectFull: Digital technology
        Type: general
      – SubjectFull: Proof of concept
        Type: general
    Titles:
      – TitleFull: A toolchain for strategy synthesis with spatial properties.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Basile, Davide
      – PersonEntity:
          Name:
            NameFull: ter Beek, Maurice H.
      – PersonEntity:
          Name:
            NameFull: Bussi, Laura
      – PersonEntity:
          Name:
            NameFull: Ciancia, Vincenzo
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 12
              Text: Dec2023
              Type: published
              Y: 2023
          Identifiers:
            – Type: issn-print
              Value: 14332779
          Numbering:
            – Type: volume
              Value: 25
            – Type: issue
              Value: 5/6
          Titles:
            – TitleFull: International Journal on Software Tools for Technology Transfer
              Type: main
ResultId 1