In this paper we look at regular path temporal logic, RPTL, a modal logic which combines the ability to quantify over (finite) paths described by regular expressions (a property which characterises PDL) with the addition of temporal operators. The formulation of RPTL was inspired by agent programming verification considerations. In this paper we prove the decidabilty of RPTL and establish complexity bounds on the satisfiability problem for RPTL by translating it into the theory of alternating tree automata on infinite trees.
The Decidability of RPTL
Khan;Fahad
2011
Abstract
In this paper we look at regular path temporal logic, RPTL, a modal logic which combines the ability to quantify over (finite) paths described by regular expressions (a property which characterises PDL) with the addition of temporal operators. The formulation of RPTL was inspired by agent programming verification considerations. In this paper we prove the decidabilty of RPTL and establish complexity bounds on the satisfiability problem for RPTL by translating it into the theory of alternating tree automata on infinite trees.| Campo DC | Valore | Lingua |
|---|---|---|
| dc.authority.people | Khan | it |
| dc.authority.people | Fahad | it |
| dc.collection.id.s | 71c7200a-7c5f-4e83-8d57-d3d2ba88f40d | * |
| dc.collection.name | 04.01 Contributo in Atti di convegno | * |
| dc.contributor.appartenenza | Istituto di linguistica computazionale "Antonio Zampolli" - ILC | * |
| dc.contributor.appartenenza.mi | 918 | * |
| dc.date.accessioned | 2024/02/19 18:17:08 | - |
| dc.date.available | 2024/02/19 18:17:08 | - |
| dc.date.issued | 2011 | - |
| dc.description.abstractita | In this paper we look at regular path temporal logic, RPTL, a modal logic which combines the ability to quantify over (finite) paths described by regular expressions (a property which characterises PDL) with the addition of temporal operators. The formulation of RPTL was inspired by agent programming verification considerations. In this paper we prove the decidabilty of RPTL and establish complexity bounds on the satisfiability problem for RPTL by translating it into the theory of alternating tree automata on infinite trees. | - |
| dc.description.affiliations | Univ Nottingham | - |
| dc.description.allpeople | Khan, ANAS FAHAD ASLAM; Khan, ANAS FAHAD ASLAM | - |
| dc.description.allpeopleoriginal | Khan, Fahad | - |
| dc.description.fulltext | none | en |
| dc.description.numberofauthors | 2 | - |
| dc.identifier.doi | 10.3233/978-1-60750-676-8-151 | - |
| dc.identifier.isbn | 978-1-60750-675-1 | - |
| dc.identifier.isi | WOS:000325429800013 | - |
| dc.identifier.uri | https://hdl.handle.net/20.500.14243/407582 | - |
| dc.language.iso | eng | - |
| dc.relation.conferencedate | 16/08/2911 | - |
| dc.relation.conferencename | The Fifth Starting AI Researchers' Symposium | - |
| dc.relation.firstpage | 151 | - |
| dc.relation.lastpage | 161 | - |
| dc.relation.numberofpages | 11 | - |
| dc.relation.volume | 222 | - |
| dc.subject.keywords | PDL | - |
| dc.subject.keywords | Regular Path Temporal Logic | - |
| dc.subject.keywords | Alternating Tree Automata | - |
| dc.subject.keywords | CTL | - |
| dc.subject.keywords | SimpleAPL | - |
| dc.subject.singlekeyword | PDL | * |
| dc.subject.singlekeyword | Regular Path Temporal Logic | * |
| dc.subject.singlekeyword | Alternating Tree Automata | * |
| dc.subject.singlekeyword | CTL | * |
| dc.subject.singlekeyword | SimpleAPL | * |
| dc.title | The Decidability of RPTL | en |
| dc.type.driver | info:eu-repo/semantics/conferenceObject | - |
| dc.type.full | 04 Contributo in convegno::04.01 Contributo in Atti di convegno | it |
| dc.type.miur | 273 | - |
| dc.ugov.descaux1 | 429343 | - |
| iris.isi.extIssued | 2011 | - |
| iris.isi.extTitle | The Decidability of RPTL | - |
| iris.orcid.lastModifiedDate | 2025/03/20 01:09:52 | * |
| iris.orcid.lastModifiedMillisecond | 1742429392696 | * |
| iris.sitodocente.maxattempts | 4 | - |
| iris.unpaywall.doi | 10.3233/978-1-60750-676-8-151 | * |
| iris.unpaywall.isoa | false | * |
| iris.unpaywall.journalisindoaj | false | * |
| iris.unpaywall.metadataCallLastModified | 03/04/2026 04:38:16 | - |
| iris.unpaywall.metadataCallLastModifiedMillisecond | 1775183896033 | - |
| iris.unpaywall.oastatus | closed | * |
| isi.authority.anceserie | FRONTIERS IN ARTIFICIAL INTELLIGENCE AND APPLICATIONS###0922-6389 | * |
| isi.category | EP | * |
| isi.contributor.affiliation | - | |
| isi.contributor.country | - | |
| isi.contributor.name | Fahad | - |
| isi.contributor.researcherId | P-3751-2018 | - |
| isi.contributor.subaffiliation | - | |
| isi.contributor.surname | Khan | - |
| isi.date.issued | 2011 | * |
| isi.description.abstracteng | In this paper we look at regular path temporal logic, RPTL, a modal logic which combines the ability to quantify over (finite) paths described by regular expressions (a property which characterises PDL) with the addition of temporal operators. The formulation of RPTL was inspired by agent programming verification considerations. In this paper we prove the decidabilty of RPTL and establish complexity bounds on the satisfiability problem for RPTL by translating it into the theory of alternating tree automata on infinite trees. | * |
| isi.description.allpeopleoriginal | Khan, F; | * |
| isi.document.sourcetype | WOS.ISTP | * |
| isi.document.type | Proceedings Paper | * |
| isi.document.types | Proceedings Paper | * |
| isi.identifier.doi | 10.3233/978-1-60750-676-8-151 | * |
| isi.identifier.eissn | 1879-8314 | * |
| isi.identifier.isi | WOS:000325429800013 | * |
| isi.journal.journaltitle | STAIRS 2010: PROCEEDINGS OF THE FIFTH STARTING AI RESEARCHERS' SYMPOSIUM | * |
| isi.journal.journaltitleabbrev | FRONT ARTIF INTEL AP | * |
| isi.language.original | English | * |
| isi.publisher.place | NIEUWE HEMWEG 6B, 1013 BG AMSTERDAM, NETHERLANDS | * |
| isi.relation.firstpage | 151 | * |
| isi.relation.lastpage | 161 | * |
| isi.relation.volume | 222 | * |
| isi.title | The Decidability of RPTL | * |
| Appare nelle tipologie: | 04.01 Contributo in Atti di convegno | |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
