Computer Science – Theory and Applications

This article surveys algorithmic techniques to save energy in computing environments. More specifically, we address power-down mechanisms as well as dynamic speed scaling in modern microprocessors. We study basic problems and present important results developed over the past years.

We introduce the notion of sofic tree-shifts which corresponds to symbolic dynamical systems of infinite trees accepted by finite tree automata. We show that, contrary to shifts of infinite sequences, there is no unique minimal deterministic irreducible tree automaton accepting an irreducible sofic tree-shift, but that there is a unique synchronized one, called the Shannon cover of the tree-shift. We define the notion of almost finite type tree-shift which is a meaningful intermediate dynamical class in between irreducible finite type tree-shifts and irreducible sofic tree-shifts. We characterize the Shannon cover of an almost finite type tree-shift and we design an algorithm to check whether a sofic tree-shift is almost of finite type.

We consider the refinement-based process for the development of security protocols. Our approach is based on the Event B refinement, which makes proofs easier and which makes the design process faithfull to the structure of the protocol as

the designer thinks of it

. We introduce the notion of mechanism related to a given security property; a mechanism can be combined with another mechanism through the double refinement process ensuring the preservation of previous security properties of mechanisms. Mechanisms and combination of mechanisms are based on

Event B

models related to the security property of the current mechanism. Analysing cryptographic protocols requires precise modelling of the attacker’s knowledge and the attacker’s behaviour conforms to the Dolev-Yao model.

We prove that, unless P = NP, no polynomial-time algorithm can approximate the minimum length of synchronizing words for a given synchronizing automaton within a constant factor.

We introduce dynamic communicating automata (DCA), an extension of communicating finite-state machines that allows for dynamic creation of processes. Their behavior can be described as sets of message sequence charts (MSCs). We consider the realizability problem for DCA: given a dynamic MSC grammar (a high-level MSC specification), is there a DCA defining the same set of MSCs? We show that this problem is decidable in doubly exponential time, and identify a class of realizable grammars that can be implemented by

finite

DCA.

In this paper, we deal with the problem of finding quasi-independent sets in graphs. This problem is formally defined in three versions, which are shown to be polynomially equivalent. The one that looks most general, namely,

f

-QIS, consists of, given a graph and a non-decreasing function

f

, finding a maximum size subset

Q

of the vertices of the graph, such that the number of edges in the induced subgraph is less than or equal to

f

(|

Q

|). For this problem, we show an exact solution method that runs within time

$O^*(2^{\frac{d-27/23}{d+1}n})$

on graphs of average degree bounded by

d

. For the most specifically defined

γ

-QIS and

k

-QIS problems, several results on complexity and approximation are shown, and greedy algorithms are proposed, analyzed and tested.

In this paper, we study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In this framework each player aims at reaching his own goal as soon as possible. We prove existence of finite-memory Nash (resp. secure) equilibria in multiplayer (resp. two-player) games.

A language

L

is prefix-closed if, whenever a word

w

is in

L

, then every prefix of

w

is also in

L

. We define suffix-, factor-, and subword-closed languages in an analogous way, where by subword we mean subsequence. We study the quotient complexity (usually called state complexity) of operations on prefix-, suffix-, factor-, and subword-closed languages. We find tight upper bounds on the complexity of the subword-closure of arbitrary languages, and on the complexity of boolean operations, concatenation, star, and reversal in each of the four classes of closed languages. We show that repeated application of positive closure and complement to a closed language results in at most four distinct languages, while Kleene closure and complement gives at most eight.

In this paper, we introduce a notion of a right-sequential function on infinite words. The main result is that any rational function is the composition of a right-sequential function and a left-sequential function. This extends a classical result of Elgot and Mezei on finite words to infinite words. We also show that our class of right-sequential functions includes the normalization of real numbers in some base and the truth value of linear temporal logic. Finally, we apply the decomposition theorem to show that automatic sequences are preserved by rational letter-to-letter functions.

Preprocessing (data reduction or kernelization)

as a strategy of coping with hard problems is universally used in almost every implementation. The history of preprocessing, like applying reduction rules simplifying truth functions, can be traced back to the 1950’s [6]. A natural question in this regard is how to measure the quality of preprocessing rules proposed for a specific problem. For a long time the mathematical analysis of polynomial time preprocessing algorithms was neglected. The basic reason for this anomaly was that if we start with an instance

I

of an NP-hard problem and can show that in polynomial time we can replace this with an equivalent instance

I

′ with |

I

′| < |

I

| then that would imply P=NP in classical complexity.

We study one-head machines through symbolic and topological dynamics. In particular, a subshift is associated to the subshift, and we are interested in its complexity in terms of realtime recognition. We emphasize the class of one-head machines whose subshift can be recognized by a deterministic pushdown automaton. We prove that this class corresponds to particular restrictions on the head movement, and to equicontinuity in associated dynamical systems.

We show that a logical framework, based around a fragment of existential second-order logic formerly proposed by others so as to capture the class of polynomially-bounded

P

-optimisation problems, cannot hope to do so, under the assumption that

P

 ≠ 

NP

. We do this by exhibiting polynomially-bounded maximisation and minimisation problems that can be expressed in the framework but whose decision versions are

NP

-complete. We propose an alternative logical framework, based around inflationary fixed-point logic, and show that we can capture the above classes of optimisation problems. We use the inductive depth of an inflationary fixed-point as a means to describe the objective functions of the instances of our optimisation problems.

Let

π

′

w

denote the failure function of the Knuth-Morris-Pratt algorithm for a word

w

. In this paper we study the following problem: given an integer array

A

′[1 ..

n

], is there a word

w

over an arbitrary alphabet Σ such that

A

′[

i

] = 

π

′

w

[

i

] for all

i

? Moreover, what is the minimum cardinality of Σ required? We give an elementary and self-contained

$\mathcal{O}(n\log n)$

time algorithm for this problem, thus improving the previously known solution [8] with no polynomial time bound. Using both deeper combinatorial insight into the structure of

π

′ and more advanced tools, we further improve the running time to

$\mathcal{O}(n)$

.

Separating words with automata is a longstanding open problem in combinatorics on words. In this paper we present a related algebraic problem. What is the minimal length of a nontrivial identical relation in the symmetric group

S

n

?

Our main contribution is an upper bound

$2^{O(\sqrt n\log n)}$

on the length of the shortest nontrivial identical relation in

S

n

. We also give lower bounds for words of a special types. These bounds can be applied to the problem of separating words by reversible automata. In this way we obtain an another proof of the Robson’s square root bound.

We present the first linear time algorithm for

d

-list colouring of a graph—i.e. a proper colouring of each vertex

v

by colours coming from lists

$\mathcal{L}(v)$

of sizes at least

deg

(

v

). Previously, procedures with such complexity were only known for Δ-list colouring, where for each vertex

v

one has

$|\mathcal{L}(v)|\geq\Delta$

, the maximum of the vertex degrees. An implementation of the procedure is available.

We prove a new completeness theorem for

topologic,

a particular system for reasoning about knowledge and topology. In fact, we show that

topologic

is complete with respect to the Cantor space, i.e., the set of all infinite 0-1-sequences endowed with the initial segment topology. To this end, we make use of the connection between the semantics of

topologic

and McKinsey and Tarski’s topological interpretation of the modal box operator, as well as of Georgatos’ Normal Form Lemma.

Computer science was born with the formal definition of the notion of an algorithm. This definition provides clear limits of automatization, separating problems into algorithmically solvable problems and algorithmically unsolvable ones. The second big bang of computer science was the development of the concept of computational complexity. People recognized that problems that do not admit efficient algorithms are not solvable in practice. The search for a reasonable, clear and robust definition of the class of practically solvable algorithmic tasks started with the notion of the class

${\mathcal{P}}$

and of

${\mathcal{NP}}$

-completeness. In spite of the fact that this robust concept is still fundamental for judging the hardness of computational problems, a variety of approaches was developed for solving instances of

${\mathcal{NP}}$

-hard problems in many applications. Our 40-years short attempt to fix the fuzzy border between the practically solvable problems and the practically unsolvable ones partially reminds of the never-ending search for the definition of “life” in biology or for the definitions of matter and energy in physics. Can the search for the formal notion of “practical solvability” also become a never-ending story or is there hope for getting a well-accepted, robust definition of it? Hopefully, it is not surprising that we are not able to answer this question in this invited talk. But to deal with this question is of crucial importance, because only due to enormous effort scientists get a better and better feeling of what the fundamental notions of science like life and energy mean. In the flow of numerous technical results, we must not forget the fact that most of the essential revolutionary contributions to science were done by defining new concepts and notions.

Let

k

be a natural number. A graph is

k

-distance hereditary if it has a tree-decomposition such that every cutmatrix has a block structure that is some submatrix of

where

I

k

is the

k

×

k

identity matrix. We characterize

k

-distance hereditary graphs and we show that for fixed

k

there exists an

O

(

n

3

) time algorithm that recognizes the graphs in this class.

We prove an exponential lower bound on the average time of inverting Goldreich’s function by

drunken

[AHI05] backtracking algorithms; therefore we resolve the open question stated in [CEMT09]. The Goldreich’s function [Gol00] has

n

binary inputs and

n

binary outputs. Every output depends on

d

inputs and is computed from them by the fixed predicate of arity

d

. Our Goldreich’s function is based on an expander graph and on the nonliniar predicates of a special type. Drunken algorithm is a backtracking algorithm that somehow chooses a variable for splitting and randomly chooses the value for the variable to be investigated at first. Our proof technique significantly simplifies the one used in [AHI05] and in [CEMT09].

The Hamiltonian cycle problem (HCP) is an important combinatorial problem with applications in many areas. While thorough theoretical and experimental analyses have been made on the HCP in undirected graphs, little is known for the HCP in directed graphs (DHCP). The contribution of this work is an effective algorithm for the DHCP. Our algorithm explores and exploits the close relationship between the DHCP and the Assignment Problem (AP) and utilizes a technique based on Boolean satisfiability (SAT). By combining effective algorithms for the AP and SAT, our algorithm significantly outperforms previous exact DHCP algorithms including an algorithm based on the award-winning Concorde TSP algorithm.

We use algorithmic tools for graphs of small treewidth to address questions in complexity theory. For both arithmetic and Boolean circuits, we show that any circuit of size

n

O

(1)

and treewidth

O

(log

i

n

) can be simulated by a circuit of width

O

(log

i

 + 1

n

) and size

n

c

, where

c

 = 

O

(1), if

i

 = 0, and

c

 = 

O

(loglog

n

) otherwise. For our main construction, we prove that multiplicatively disjoint arithmetic circuits of size

n

O

(1)

and treewidth

k

can be simulated by bounded fan-in arithmetic formulas of depth

O

(

k

2

log

n

). From this we derive an analogous statement for syntactically multilinear arithmetic circuits, which strengthens the central theorem of [14]. As another application, we derive that constant width arithmetic circuits of size

n

O

(1)

can be balanced to depth

O

(log

n

), provided certain restrictions are made on the use of iterated multiplication. Also from our main construction, we derive that Boolean bounded fan-in circuits of size

n

O

(1)

and treewidth

k

can be simulated by bounded fan-in formulas of depth

O

(

k

2

log

n

). This strengthens in the non-uniform setting the known inclusion that SC

0

 ⊆ NC

1

. Finally, we apply our construction to show that

Reachability

and

Circuit Value Problem

for some treewidth restricted cases can be solved in LogDCFL.

A colouring of a graph is ecological if every pair of vertices that have the same set of colours in their neighbourhood are coloured alike. We consider the following problem: if a graph

G

and an ecological colouring

c

of

G

are given, can further vertices added to

G

, one at a time, be coloured using colours from some finite set

C

so that at each stage the current graph is ecologically coloured? If the answer is yes, then we say that the pair (

G

,

c

) is ecologically online extendible. By generalizing the well-known First-Fit algorithm, we are able to characterize when (

G

,

c

) is ecologically online extendible. For the case where

c

is a colouring of

G

in which each vertex is coloured distinctly, we give a simple characterization of when (

G

,

c

) is ecologically online extendible using only the colours of

c

, and we also show that (

G

,

c

) is always online extendible if we permit ourselves to use one extra colour. We also study (off-line) ecological

H

-colourings where the colouring must satisfy further restrictions imposed by some fixed pattern graph

H

. We characterize the computational complexity of this problem. This solves an open question posed by Crescenzi et al.

Quantum computing is widely regarded as being able to offer computational complexity benefits beyond the possibilities of classical computing. Yet the relationship of quantum to classical computational complexity is little understood. A fundamental approach to exploring this issue is to study the extent to which quantum computations (especially with restricted sub-universal ingredients) can be classically efficiently simulated. We will discuss a series of results relating to the classical simulation of some interesting classes of quantum computations, particularly Clifford circuits, matchgate circuits and a simple class of quantum circuits (so-called IQP circuits) comprising commuting gates. We will outline an argument that a suitably efficient classical simulation of the latter class would imply a collapse of the polynomial hierarchy.

In this paper we compare two types of conditional prefix complexity assuming that conditions are sets of strings rather than [4] strings. We show that prefix-free and prefix-correct versions of the definition are essentially different.

We define monotone complexity

${\textit{KM}}(x,y)$

of a pair of binary strings

x

,

y

in a natural way and show that

${\textit{KM}}(x,y)$

may exceed the sum of the lengths of

x

and

y

(and therefore the a priori complexity of a pair) by

α

log(|

x

| + |

y

|) for every

α

< 1 (but not for

α

> 1).

We also show that decision complexity of a pair or triple of strings does not exceed the sum of its lengths.

Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics. We propose symbolic models for single-conclusion proof logics (

FLP

and its extensions). The corresponding soundness and completeness theorems are proven. The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization. In particular, we construct an extension of

FLP

that enjoys the strong proof internalization property with empty context.

We show that the problem of checking careful synchronizability of partial finite automata and the problem of finding the shortest carefully synchronizing word are PSPACE-complete. We show that the problem of checking

D

1

,

D

2

and

D

3

-directability of nondeterministic finite automata and the problem of finding the shortest

D

1

,

D

2

and

D

3

-directing word are PSPACE-complete. The restrictions of these problems to 2-letter automata remain PSPACE-complete.

The known algorithms for linear systems of equations perform significantly slower where the input matrix is ill conditioned, that is lies near a matrix of a smaller rank. The known methods counter this problem only for some important but special input classes, but our novel randomized augmentation techniques serve as a remedy for a typical ill conditioned input and similarly facilitates computations with rank deficient input matrices. The resulting acceleration is dramatic, both in terms of the proved bit-operation cost bounds and the actual CPU time observed in our tests. Our methods can be effectively applied to various other fundamental matrix and polynomial computations as well.

The predicate logic of recursive realizability was carefully studied by the author in the 1970s. In particular, it was proved that the predicate realizability logic changes if the basic language of formal arithmetic is replaced by its extension with the truth predicate. In the paper this result is generalized by considering similar extensions of the arithmetical language by transfinite induction up to an arbitrary constructive ordinal. Namely, for every constructive ordinal

α

, a transfinite sequence of extensions

LA

β

(

β

 ≤ 

α

) of the first-order language of formal arithmetic is considered. Constructive semantics for these languages is defined in terms of recursive realizability. Variants of

LA

β

-realizability for the predicate formulas are considered and corresponding predicate logics are studied.

By blending principles from mechanism design, algorithms, machine learning and massive distributed computing, the search industry has become good at optimizing monetization on sound scientific principles. This represents a successful and growing partnership between computer science and microeconomics. When it comes to understanding how online users respond to the content and experiences presented to them, we have more of a lacuna in the collaboration between computer science and certain social sciences. We will use a concrete technical example from image search results presentation, developing in the process some algorithmic and machine learning problems of interest in their own right. We then use this example to motivate the kinds of studies that need to grow between computer science and the social sciences; a critical element of this is the need to blend large-scale data analysis with smaller-scale eye-tracking and “individualized” lab studies.

Given a directed graph

G

 = (

V

,

A

), the

Directed Maximum Leaf Spanning Tree

problem asks to compute a directed spanning tree with as many leaves as possible. By designing a branching algorithm analyzed with

Measure&Conquer

, we show that the problem can be solved in time

${\mathcal{O}}^*({1.9044}^n)$

using polynomial space. Allowing exponential space, this run time upper bound can be lowered to

${\mathcal{O}}^*(1.8139^n)$

.

The underlying question of propositional proof complexity is amazingly simple: when interesting propositional tautologies possess efficient (which usually means short) proofs in a given propositional proof system? This theory is extremely well connected to very different disciplines like computational complexity, theoretical cryptography, automated theorem proving, mathematical logic, algebra and geometry. And, given its mixed origins, methods and concepts employed in the area are also very diverse.

Many classical search problems can be cast in the following abstract framework: Given a finite set

X

and a subset

M

 ⊆ 

X

of marked elements,

detect

if

M

is empty or not, or

find

an element in

M

if there is any. When

M

is not empty, a naive approach to the finding problem is to repeatedly pick a uniformly random element of

X

until a marked element is sampled. A more sophisticated approach might use a Markov chain, that is a random walk on the state space

X

in order to generate the samples. In that case the resources spent for previous steps are often reused to generate the next sample. Random walks also model spatial search in physical regions where the possible moves are expressed by the edges of some specific graph. The

hitting time

of a Markov chain is the number of steps necessary to reach a marked element, starting from the stationary distribution of the chain.

In this survey we compare the similarities, differences and the complexities of two very different approaches to solve a general constraint satisfaction probblems (CSP). One is the algorithm used in Moser’s ingenious proof of a constructive version of Lovász Local Lemma [3], the other is the

k

-SAT random walk algorithm from [5,6], generalized to CSP’s. There are several similarities, both algorithms use a version of stochastic local search (SLS), but the kind of local search neighborhood is defined differently, also the preconditions for the algorithms to work (efficiently) are quite different.

We study growth properties of power-free languages over finite alphabets. We consider the function

α

(

k

,

β

) whose values are the exponential growth rates of

β

-power-free languages over

k

-letter alphabets and clarify its asymptotic behaviour. Namely, we suggest the laws of the asymptotic behaviour of this function when

k

tends to infinity and prove some of them as theorems. In particular, we obtain asymptotic formulas for

α

(

k

,

β

) for the case

β

 ≥ 2.

Given a finite directed graph, a coloring of its edges turns the graph into a finite-state automaton. A

k

-synchronizing word of a deterministic automaton is a word in the alphabet of colors at its edges that maps the state set of the automaton at least on

k

-element subset. A coloring of edges of a directed strongly connected finite graph of a uniform outdegree (constant outdegree of any vertex) is

k

-synchronizing if the coloring turns the graph into a deterministic finite automaton possessing a

k

-synchronizing word.

For

k

 = 1 one has the well known road coloring problem. The recent positive solution of the road coloring problem implies an elegant generalization considered first by Béal and Perrin: a directed finite strongly connected graph of uniform outdegree is

k

-synchronizing iff the greatest common divisor of lengths of all its cycles is

k

.

Some consequences for coloring of an arbitrary finite digraph are presented. We describe a subquadratic algorithm of the road coloring for the

k

-synchronization implemented in the package TESTAS. A new linear visualization program demonstrates the obtained coloring. Some consequences for coloring of an arbitrary finite digraph and of such a graph of uniform outdegree are presented.

When we represent a decision problem, like CIRCUIT-SAT, as a language over the binary alphabet, we usually do not specify how to encode instances by binary strings. This relies on the empirical observation that the truth of a statement of the form “CIRCUIT-SAT belongs to a complexity class

C

” does not depend on the encoding, provided both the encoding and the class

C

are “natural”. In this sense most of the Complexity theory is “encoding invariant”.

The notion of a polynomial time computable distribution from Average Case Complexity is one of the exceptions from this rule. It might happen that a distribution over some objects, like circuits, is polynomial time computable in one encoding and is not polynomial time computable in the other encoding. In this paper we suggest an encoding invariant generalization of a notion of a polynomial time computable distribution. The completeness proofs of known distributional problems, like Bounded Halting, are simpler for the new class than for polynomial time computable distributions.

This paper has no new technical contributions. All the statements are proved using the known techniques.

By terms-allowed-in-types capacity, the Logic of Proofs

$\textbf{LP}$

enjoys a system of advanced combinatory terms, while including types of the form

t

:

φ

(

t

), which have self-referential meanings. This paper suggests a research on possible

$\textbf{S4}$

measures of self-referentiality introduced by this capacity. Specifically, we define “prehistoric phenomena” in

$\textbf{G3s}$

, a Gentzen-style formulation of modal logic

$\textbf{S4}$

. A special phenomenon, namely, “left prehistoric loop”, is then shown to be necessary for self-referentiality in realizations of

$\textbf{S4}$

theorems in

$\textbf{LP}$

.