Search

This paper introduces Graded Computation Tree Logic with finite path semantics (GCTL f ⁎ , for short), a variant of Computation Tree Logic CTL⁎, in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTL f ⁎ are interpreted over Kripke structures. The syntax of GCTL f ⁎ has path quantifiers of the form E ≥ g ψ which express that there are at least g many distinct finite paths that satisfy ψ. After defining and justifying the logic GCTL f ⁎ , we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTL f ⁎ under the imperfect information setting. Precisely, we introduce GCTLK f ⁎ , an epistemic extension of GCTL f ⁎ and prove that the model checking problem also in this case is PSPACE-complete. [ABSTRACT FROM AUTHOR]

Although there have been many works on bounded semantics, a characterization of a good definition for a bounded semantics has not been given, and this has led to definitions of bounded semantics of temporal logics that may not be appropriate with respect to the potential usefulness as a basis for developing bounded model checking approaches. On the other side, the research effort on bounded semantics has mainly focused on existentially interpreted fragments of temporal logics, due to the intricacy of defining appropriate bounded semantics for universally interpreted fragments, or for temporal logics with path quantifiers that are closed under negation. This work addresses these two problems, by defining the characteristics of bounded semantics for clarifying the concept of bounded semantics, and presenting a bounded semantics for the full set of CTL, a logic closed under negation, including possibility for specifying both existential and universal properties. [ABSTRACT FROM AUTHOR]

Abstract: Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one. Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. In this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution. [Copyright &y& Elsevier]

Abstract: We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of where subscripts put quantitative constraints on the time it takes before a property is satisfied. We exhibit an important gap between logics where subscripts of the form “” (exact duration) are allowed, and simpler logics that only allow subscripts of the form “” or “” (bounded duration). Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes -complete or -complete depending on the considered semantics. [Copyright &y& Elsevier]