A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information

Autor:	Aline Maria Santos Andrade, Jandson S. Ribeiro
Rok vydání:	2015
Předmět:	Model checking TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computation tree logic Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Kripke models Modal transition system Specific model Contraction (operator theory) Algorithm
Zdroj:	Formal Methods and Software Engineering ISBN: 9783319254227 ICFEM
DOI:	10.1007/978-3-319-25423-4_6
Popis:	In this work we address the problem of model checking a desired property specified in Computation Tree Logic (CTL) in the presence of partial information. The Kripke Modal Transition System (KMTS) is used for modelling due its capacity to represent indefinitions explicitly which enables a KMTS interpretation as a set of Kripke structures. In this interpretation a specific model checking algorithm is required that can return one of the three possible values: true when all Kripke models of the set satisfy the property, false when no Kripke models of the set satisfy the property and indefinite when some models satisfy and others do not. To the best of our knowledge the literature lacks a KMTS model checking algorithm that fits this interpretation and in this paper we present an algorithm based on a game approach called a Contraction Model Checking algorithm for this purpose.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::d6fcad638892f5474970db10c15dc779 https://doi.org/10.1007/978-3-319-25423-4_6 Zobrazit plný text záznamu