International Journal of Foundations of Computer Science

Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous temporal logic for intervals studied so far is probably Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments are undecidable. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider here different combinations of the interval relations begins (B), meets (A), later (L) and their inverses , and . We know from previous work that the combination is decidable only when finite domains are considered (and undecidable elsewhere), and that is decidable over the natural numbers. In the present paper we show that, over strongly discrete linear models (e.g. finite orders, the naturals, the integers), decidability of can be further extended to capture the language , which lies strictly in between and . The logic turns out to be maximal w.r.t decidability over the considered classes, and its satisfiability problem is EXPSPACE-complete. In this paper we also provide an optimal non-deterministic decision procedure, and we show that the language is powerful enough to polynomially encode metric constraints on the length of the current interval.

We design a novel algorithm for solving Mean-Payoff Games (MPGs). Besides solving an MPG in the usual sense, our algorithm computes more information about the game, information that is important with respect to applications. The weights of the edges of an MPG can be thought of as a gained/consumed energy – depending on the sign. For each vertex, our algorithm computes the minimum amount of initial energy that is sufficient for player Max to ensure that in a play starting from the vertex, the energy level never goes below zero. Our algorithm is not the first algorithm that computes the minimum sufficient initial energies, but according to our experimental study it is the fastest algorithm that computes them. The reason is that it utilizes the strategy improvement technique which is very efficient in practice.

We introduce two-level discounted and mean-payoff games played by two players on a perfect-information stochastic game graph. The upper level game is a discounted or mean-payoff game and the lower level game is a (undiscounted) reachability game. Two-level games model hierarchical and sequential decision making under uncertainty across different time scales.

For both discounted and mean-payoff two-level games, we show the existence of pure memoryless optimal strategies for both players and an ordered field property. We show that if there is only one player (Markov decision processes), then the values can be computed in polynomial time. It follows that whether the value of a player is equal to a given rational constant in two-level discounted or mean-payoff games can be decided in NP ∩ coNP. We also give an alternate strategy improvement algorithm to compute the value.

This paper is a continuation and correction of a paper presented by the same authors at the conference GANDALF 2010. We consider the Modal μ-calculus and some fragments of it. For every positive integer k we consider the class SCCk of all finite graphs whose strongly connected components have size at most k, and the class TWk of all finite graphs of tree width at most k. As upper bounds, we show that for every k, the temporal logic CTL* collapses to alternation free μ-calculus in SCCk; and in TW1, the winning condition for parity games of any index n belongs to the level Δ₂ of Modal μ-calculus. As lower bounds, we show that Büchi automata are not closed under complement in TW2 and coBüchi nondeterministic and alternating automata differ in TW1.

This work considers a finite-duration variant of Muller games, and their connection to infinite-duration Muller games. In particular, it studies the question of how long a finite-duration Muller game must be played before the winner of the finite-duration game is guaranteed to be able to win the corresponding infinite-duration game. Previous work by McNaughton has shown that this must occur after moves, and the reduction from Muller games to parity games gives a bound of n · n! + 1 moves. We improve upon both of these results, by giving a bound of 3ⁿ moves.

The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parity game are strategy iteration algorithms. These are global in nature since they require the entire parity game to be present at the beginning. This is a distinct disadvantage because in many applications one only needs to know which winning region a particular node belongs to, and a witnessing winning strategy may cover only a fractional part of the entire game graph.

We present two local strategy iteration algorithms which explore the game graph on-the-fly whilst performing the improvement steps. We also compare them empirically with existing global strategy iteration algorithms and the currently only other local algorithm for solving parity games. It turns out that local strategy iteration can outperform these others significantly.

We examine perfect information stochastic mean-payoff games – a class of games containing as special sub-classes the usual mean-payoff games and parity games. We show that deterministic memoryless strategies that are optimal for discounted games with state-dependent discount factors close to 1 are optimal for priority mean-payoff games establishing a strong link between these two classes.

Systems of parallel finite automata communicating by states are investigated. We consider deterministic and nondeterministic devices and distinguish four working modes. It is known that systems in the most general mode are as powerful as one-way multi-head finite automata. Here we solve some open problems on the computational capacity of systems working in the remaining modes. In particular, it is shown that deterministic returning and non-returning devices are equivalent, and that there are languages which are accepted by deterministic returning and centralized systems but cannot be accepted by deterministic non-returning centralized systems. Furthermore, we show that nondeterministic systems are strictly more powerful than their deterministic variants in all the four working modes. Finally, incomparability with the classes of (deterministic) (linear) context-free languages as well as the Church-Rosser languages is derived.

HAS-160, a Korean hash standard, has been widely used in the Korean industry. This paper aims to re-evaluate the security of HAS-160 in the encryption mode, a block cipher with the 512-bit key size and the 160-bit plaintext block size. A previous attack is based on a 71-round related-key distinguisher with probability 2^-304. Using some delicate properties of HAS-160 and employing a bit-fixing technique, we present a 72-round related-key rectangle distinguisher with probability 2^-290 in this paper. Based on this new distinguisher, two key recovery attacks on the encryption mode of the full 80-round HAS-160 are performed, which improve the earlier results. The attacks presented in this paper are the best known results on HAS-160 in the encryption mode in terms of the number of attack rounds and the efficiency of attacks.

Vectorial Boolean functions play an important role in cryptography. How to construct vectorial Boolean functions with good cryptographic properties is a nice problem that worth to be investigated. In this paper we present several constructions of balanced vectorial Boolean functions with high algebraic immunity, high(or optimum) algebraic degree, and very high nonlinearity. In some cases, the constructed functions also achieve optimum algebraic immunity.