Wyniki wyszukiwania - BazTech

1

Graded Alternating-Time Temporal Logic

Faella M., Napoli M., Parente M.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

189-210

EN

Recently, temporal logics such as μ-calculus and Computational Tree Logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Both μ-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. We extend the Alternating-time Temporal Logic (ATL) introduced by Alur et al., that is a derivative of CTL interpreted on game structures, rather than transition systems. We solve the model-checking problem in the concurrent and turn-based settings, proving its PTIME-completeness. We present, and compare with each other, two different semantics: the first seems suitable to off-line synthesis applicationswhile the secondmay find application in the verification of fault-tolerant controllers. We also study the case where players can only employ memoryless strategies, showing that also in this case the model-checking problem is in PTIME.

2

Model Checking for Graded CTL

Ferrante A., Napoli M., Parente M.

Fundamenta Informaticae

|

2009

|

Vol. 96, nr 3

323-339

EN

Recently, complexity issues related to the decidability of the μ-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi ([19]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of at least k or all but k, for a non-negative integer k. In this paper we study the Computational Tree Logic CTL, a branching time extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure K and give an algorithm to solve the model-checking problem running in time [...] which is hence tight for the problem (here φ is the number of temporal and boolean operators and does not include the values occurring in the graded modalities). In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples to a specification φgiven in CTL. However, these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both NP-hard and coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of graded-CTL, and have proved that the model-checking problem is solvable in polynomial time.

3

Synchronization of a line of identical processors at a given time

La Torre S., Napoli M., Parente D.

Fundamenta Informaticae

|

1998

|

Vol.34, nr 1,2

103-128

EN

We are given a line of n identical processors (finite automata) that work synchronously. Each processor can transmit just one bit of information to the adjacent processor (if any) to the left and to the right. The computation starts at time 1 with the leftmost processor in an initial atate and all other processors in a quiescent state. Given the time f(n), the problem is to set (synchronize) all the processors in a particular state for the first time, at the very same instant f(n). This problem is also known as the Firing Squad Synchronization Problem and was introduced by Moore in 1964. Mazoyer has given a minimal time solution with the least number of different states (six) and very recently he has given a minimal time solution for the constrained problem in which adjacent processors can exchange only one bit. In this paper we present solutions that synchronize the line a given time, expressed as a function of n. In particular we give solutions that synchronize at the times n log n, nÖn, n2 and 2n. Moreover we also show how to compose solutions in such a way to obtain synchronizing solutions for all times expressed by polynomials with nonnegative coefficients. Clearly all such solutions work also in the general case when the bit constraint is relaxed.