Model-checking games for fixpoint logics with partial order modelsReportar como inadecuado




Model-checking games for fixpoint logics with partial order models - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Reference: Gutierrez, J and Bradfield, J, (2009). Model-checking games for fixpoint logics with partial order models.Citable link to this page:

 

Model-checking games for fixpoint logics with partial order models

Abstract: We introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the one-step interleaving semantics of such models is not considered, some problems that may arise when using interleaving semantics are avoided and new decidability results for partial orders are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus (Lμ), in a noninterleaving setting they verify properties of Separation Fixpoint Logic (SFL), a logic that can specify in partial orders properties not expressible with Lμ. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving previous results in the literature.

Peer Review status:Peer reviewedPublication status:PublishedVersion:Accepted ManuscriptConference Details: CONCUR 2009 - Concurrency Theory : 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. ProceedingsNotes:Copyright © Springer-Verlag Berlin Heidelberg 2009. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-04081-8_24.

Bibliographic Details

Publisher: Springer Berlin Heidelberg

Publisher Website: http://www.springer.com/

Host: CONCUR 2009 - Concurrency Theory : 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedingssee more from them

Publication Website: http://link.springer.com/book/10.1007/978-3-642-04081-8

Issue Date: 2009

pages:354-368Identifiers

Urn: uuid:e476c283-3e9e-48f1-8b6c-bb151a9fa458

Isbn: 978-3-642-04080-1

Isbn: 978-3-642-04081-8

Source identifier: 572659

Doi: https://doi.org/10.1007/978-3-642-04081-8_24

Issn: 0302-9743 Item Description

Type: Conference;

Version: Accepted ManuscriptKeywords: modal and temporal logics model-checking games Hintikka game semantics partial order models of concurrency process algebras Tiny URL: pubs:572659

Relationships





Autor: Gutierrez, J - institutionUniversity of Oxford Oxford, MPLS, Computer Science - - - Bradfield, J - - - - Bibliographic Details Pu

Fuente: https://ora.ox.ac.uk/objects/uuid:e476c283-3e9e-48f1-8b6c-bb151a9fa458



DESCARGAR PDF




Documentos relacionados