Umeå universitets logga

umu.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces
Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap. 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 (Engelska)Ingår i: IJCAI International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence , 2022, s. 2553-2560Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
International Joint Conferences on Artificial Intelligence , 2022. s. 2553-2560
Serie
International Joint Conference on Artificial Intelligence, ISSN 1045-0823
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:umu:diva-203074DOI: 10.24963/ijcai.2022/354Scopus ID: 2-s2.0-85133201271ISBN: 978-1-956792-00-3 (digital)OAI: oai:DiVA.org:umu-203074DiVA, id: diva2:1727773
Konferens
31st International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna 23-29 July 2022
Tillgänglig från: 2023-01-17 Skapad: 2023-01-17 Senast uppdaterad: 2023-01-17Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

Calvanese, Diego

Sök vidare i DiVA

Av författaren/redaktören
Calvanese, Diego
Av organisationen
Institutionen för datavetenskap
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 131 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf