References of "Information & Computation"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailThe freeness problem over matrix semigroups and bounded languages
Charlier, Emilie ULg; Honkala, Juha

in Information & Computation (2013)

We study the freeness problem for matrix semigroups. We show that the freeness problem is decidable for upper-triangular 2 × 2 matrices with rational entries when the products are restricted to certain ... [more ▼]

We study the freeness problem for matrix semigroups. We show that the freeness problem is decidable for upper-triangular 2 × 2 matrices with rational entries when the products are restricted to certain bounded languages. [less ▲]

Detailed reference viewed: 6 (2 ULg)
Full Text
Peer Reviewed
See detailModule checking
Kupferman, Orna; Vardi, Moshe Y; Wolper, Pierre ULg

in Information & Computation (2001), 164(2), 322-344

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that ... [more ▼]

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems. (C) 2001 Academic Press. [less ▲]

Detailed reference viewed: 36 (8 ULg)
Full Text
Peer Reviewed
See detailReasoning about Infinite Computations
Vardi, Moshe Y.; Wolper, Pierre ULg

in Information & Computation (1994), 115(1), 1-37

We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions ... [more ▼]

We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions (finite, looping, and repeating) for the automata. It turns out, however that these logics all have the same expressive power and that their decision problems are all PSPACE-complete. We also investigate connectives defined by alternating automata and show that they do not increase the expressive power of the logic or the complexity of the decision problem. (C) 1994 Academic Press, Inc. [less ▲]

Detailed reference viewed: 52 (0 ULg)
Peer Reviewed
See detailA Partial Approach To Model Checking
Godefroid, Patrice; Wolper, Pierre ULg

in Information & Computation (1994), 110(2), 305--326

Detailed reference viewed: 8 (1 ULg)