Umeå University's logo

umu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces
Umeå University, Faculty of Science and Technology, Department of Computing Science. Free University of Bozen-Bolzano, Italy.ORCID iD: 0000-0001-5174-9693
Sapienza University of Rome, Italy.
Free University of Bozen-Bolzano, Italy.
Sapienza University of Rome, Italy.
2022 (English)In: IJCAI International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence , 2022, p. 2553-2560Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of model checking first-order dynamic systems where new objects can be injected in the active domain during execution. Notable examples are systems induced by a first-order action theory expressed, e.g., in the situation calculus. Recent results show that, under state-boundedness, such systems, in spite of having a first-order representation of the state, admit decidable model checking for full first-order mu-calculus. However, interestingly, model checking remains undecidable in the case of first-order LTL (LTL-FO). In this paper, we show that in LTL-FOp, the fragment of LTL-FO where quantification ranges only over objects that persist along traces, model checking state-bounded systems becomes decidable over infinite and finite traces. We then employ this result to show how to handle monitoring of LTL-FOp properties against a trace stemming from an unknown state-bounded dynamic system, simultaneously considering the finite trace up to the current point, and all its possibly infinite future continuations.

Place, publisher, year, edition, pages
International Joint Conferences on Artificial Intelligence , 2022. p. 2553-2560
Series
International Joint Conference on Artificial Intelligence, ISSN 1045-0823
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:umu:diva-203074DOI: 10.24963/ijcai.2022/354Scopus ID: 2-s2.0-85133201271ISBN: 978-1-956792-00-3 (electronic)OAI: oai:DiVA.org:umu-203074DiVA, id: diva2:1727773
Conference
31st International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna 23-29 July 2022
Available from: 2023-01-17 Created: 2023-01-17 Last updated: 2023-01-17Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Calvanese, Diego

Search in DiVA

By author/editor
Calvanese, Diego
By organisation
Department of Computing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 221 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf