SOFSEM 2012: Theory and Practice of Computer Science

Alan Mathison Turing is revered among computer scientists for laying down the foundations of theoretical computer science via the introduction of the Turing machine, an abstract model of computation upon which, an elegant notion of cost and a theory of complexity can be developed. In this paper we argue that the contribution of Turing to “the other side of computer science”, namely the domain of numerical computations as pioneered by Newton, Gauss, &c, and carried out today in the name of numerical analysis, is of an equally foundational nature.

Various methods exists in the litearture for denoting the configuration of a Turing Machine. A key difference is whether the head position is indicated by some integer (mathematical representation) or is specified by writing the machine state next to the scanned tape symbol (intrinsic representation).

From a mathematical perspective this will make no difference. However, since Turing Machines are primarily used for proving undecidability and/or hardness results these representations do matter. Based on a number of applications we show that the intrinsic representation should be preferred.

We attempt to put the title problem and the Church-Turing thesis into a proper perspective and to clarify some common misconceptions related to Turing’s analysis of computation. We examine two approaches to the title problem, one well-known among philosophers and another among logicians.

Given a directed graph G, an edge is a strong bridge if its removal increases the number of strongly connected components of G. Similarly, a vertex is a strong articulation point if its removal increases the number of strongly connected components of G. Strong articulation points and strong bridges are related to the notion of 2-vertex and 2-edge connectivity of directed graphs, which surprisingly seems to have been overlooked in the past. In this talk, we survey some very recent work in this area, both from the theoretical and the practical viewpoint.

We will give plausible arguments in favor of a claim that we already have sufficient knowledge to understand the working of interesting artificial minds attaining a high-level cognition, consciousness included. Achieving a higher-level AI seems to be not a matter of a fundamental scientific breakthrough but rather a matter of exploiting our best theories of artificial minds and our most advanced data processing technologies. We list the theories we have in mind and illustrate their role and place on the example of a high-level architecture of a conscious cognitive agent with a potential to pass the Turing test.

It is time for Adaptive Web (server) extensions to grow up and become generic. The GRAPPLE (EU FP7) project aimed at integrating Learning Management Systems (LMS) with Adaptive Learning Environments (ALE) in order to support life-long learning. But instead of developing a dedicated Web-based ALE we developed an architecture containing a fully generic adaptive Web server, a distributed User Modeling Framework and a generic browser-based authoring environment for Domain Models and Conceptual Adaptation Models. The GRAPPLE architecture can be used for creating and serving any type of adaptive Web-based application. It supports content-, link- and presentation (layout) adaptation based (in any programmable way) on any desired user model information. In this paper we concentrate on GALE [21], the adaptation engine we renamed to the “Generic Adaptation Language and Engine”. We describe the key elements that make GALE into a truly generic and highly extensible Web-based adaptive delivery environment.

Similarity has been a central notion throughout our lives and due to the current unprecedented growth of digital data collections of various types in huge quantities, similarity management of digital data is becoming necessary. The Multi-Feature Indexing Network (MUFIN) is a generic engine for similarity search in various data collections, such as pictures, video, music, biometric data, sensor and scientific data, and many others. MUFIN can provide answers to queries based on the example paradigm. The system assumes a very universal concept of similarity that is based on the mathematical notion of metric space. In this concept, the data collection is seen as objects together with a method to measure similarity between pairs of objects. The key implementation strategies of MUFIN concern:

extensibility

- to be applied on variety of data types,

scalability

- to be efficient even for very large databases, and

infrastructure independence

- to run on various hardware infrastructures so that the required query response time and query execution throughput can be adjusted. The capability of MUFIN is demonstrated by several applications and advance prototypes. Other applications and future research and application trends are also to be discussed.

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification against all environments. While model-checking theory has led to industrial development and use of formal-verification tools, the integration of synthesis in the industry is slow. This has to do with theoretical limitations, like the complexity of the problem, algorithmic limitations, like the need to determinize automata on infinite words and solve parity games, methodological reasons, like the lack of satisfactory compositional synthesis algorithms, and practical reasons: current algorithms produce systems that satisfy the specification, but may do so in a peculiar way and may be larger or less well-structured than systems constructed manually.

The research community has managed to suggest some solutions to these limitations, and bring synthesis algorithms closer to practice. Significant barriers, however, remain. Moreover, the integration of synthesis in real applications has taught us that the traditional setting of synthesis is too simplified and has brought with it new algorithmic challenges. This paper introduces the synthesis problem, algorithms for solving it, and recent promising ideas in making temporal-synthesis useful in practice.

The Learning Parity with Noise (LPN) problem has recently found many applications in cryptography as the hardness assumption underlying the constructions of “provably secure” cryptographic schemes like encryption or authentication protocols. Being provably secure means that the scheme comes with a proof showing that the existence of an efficient adversary against the scheme implies that the underlying hardness assumption is wrong.

LPN based schemes are appealing for theoretical and practical reasons. On the theoretical side, LPN based schemes offer a very strong security guarantee. The LPN problem is equivalent to the problem of decoding random linear codes, a problem that has been extensively studied in the last half century. The fastest known algorithms run in exponential time and unlike most number-theoretic problems used in cryptography, the LPN problem does not succumb to known quantum algorithms. On the practical side, LPN based schemes are often extremely simple and efficient in terms of code-size as well as time and space requirements. This makes them prime candidates for light-weight devices like RFID tags, which are too weak to implement standard cryptographic primitives like the AES block-cipher.

This talk will be a gentle introduction to provable security using simple LPN based schemes as examples. Starting from pseudorandom generators and symmetric key encryption, over secret-key authentication protocols, and, if time admits, touching on recent constructions of public-key identification, commitments and zero-knowledge proofs.

Word Sense Disambiguation (WSD) and Word Sense Induction (WSI) are two fundamental tasks in Natural Language Processing (NLP), i.e., those of, respectively, automatically assigning meaning to words in context from a predefined sense inventory and discovering senses from text for a given input word. The two tasks have generally been hard to perform with high accuracy. However, today innovations in approach to WSD and WSI are promising to open up many interesting new horizons in NLP and Information Retrieval applications. This paper is a quick tour on how to start doing research in this exciting field and suggests the hottest topics to focus on.

Practical application of the Turing Test throws up all sorts of questions regarding the nature of intelligence in both machines and humans. For example - Can machines tell original jokes? What would this mean to a machine if it did so? It has been found that acting as an interrogator even top philosophers can be fooled into thinking a machine is human and/or a human is a machine - why is this? Is it that the machine is performing well or is it that the philosopher is performing badly? All these questions, and more, will be considered. Just what does the Turing test tell us about machines and humans? Actual transcripts will be considered with startling results.

This paper presents a complete account of positive and negative results on the finite axiomatizability of weak complete simulation semantics over the language BCCSP. We offer finite (un)conditional ground-complete axiomatizations for the weak complete simulation precongruence. In sharp contrast to this positive result, we prove that, in the presence of at least one observable action, the (in)equational theory of the weak complete simulation precongruence over BCCSP does not have a finite (in)equational basis. In fact, the set of (in)equations in at most one variable that hold in weak complete simulation semantics over BCCSP does not have an (in)equational basis of ‘bounded depth’, let alone a finite one.

The

Minimum Duplication

problem is a well-known problem in phylogenetics and comparative genomics. Given a set of gene trees, the

Minimum Duplication

problem asks for a species tree that induces the minimum number of gene duplications in the input gene trees. More recently, a variant of the

Minimum Duplication

problem, called

Minimum Duplication Bipartite

, has been introduced in [14], where the goal is to find all

pre-duplications

, that is duplications that precede, in the evolution, the first speciation with respect to a species tree. In this paper, we investigate the complexity of both

Minimum Duplication

and

Minimum Duplication Bipartite

problems. First of all, we prove that the

Minimum Duplication

problem is

APX

-hard, even when the input consists of five uniquely leaf-labelled gene trees (progressing on the complexity of the problem). Then, we show that the

Minimum Duplication Bipartite

problem can be solved efficiently by a randomized algorithm when the input gene trees have bounded depth.

We consider computations of a Turing machine under noise that causes consecutive violations of the machine’s transition function. Given a constant upper bound

β

on the size of bursts of faults, we construct a Turing machine

M

(

β

) subject to faults that can simulate any fault-free machine under the condition that bursts not closer to each other than

V

for an appropriate

V

 = 

O

(

β

).

Single look-ahead unit resolution (SLUR) algorithm is a nondeterministic polynomial time algorithm which for a given input formula in a conjunctive normal form (CNF) either outputs its satisfying assignment or gives up. A CNF formula belongs to the SLUR class if no sequence of nondeterministic choices causes the SLUR algorithm to give up on it. The SLUR class is reasonably large. It is known to properly contain the well studied classes of Horn CNFs, renamable Horn CNFs, extended Horn CNFs, and CC-balanced CNFs. In this paper we show that the SLUR class is considerably larger than the above mentioned classes of CNFs by proving that every Boolean function has at least one CNF representation which belongs to the SLUR class. On the other hand, we show, that given a CNF it is coNP-complete to decide whether it belongs to the SLUR class or not. Finally, we define a non-collapsing hierarchy of CNF classes SLUR(

i

) in such a way that for every fixed

i

there is a polynomial time satisfiability algorithm for the class SLUR(

i

), and that every CNF on

n

variables belongs to SLUR(

i

) for some

i

 ≤ 

n

.

We investigate the relationship between two kinds of vertex colorings of hypergraphs: unique-maximum colorings and conflict-free colorings. In a unique-maximum coloring, the colors are ordered, and in every hyperedge of the hypergraph the maximum color in the hyperedge occurs in only one vertex of the hyperedge. In a conflict-free coloring, in every hyperedge of the hypergraph there exists a color in the hyperedge that occurs in only one vertex of the hyperedge. We define corresponding unique-maximum and conflict-free chromatic numbers and investigate their relationship in arbitrary hypergraphs. Then, we concentrate on hypergraphs that are induced by simple paths in tree graphs.

The maximum number of minimal dominating sets that a graph on

n

vertices can have is known to be at most 1.7159

n

. This upper bound might not be tight, since no examples of graphs with 1.5705

n

or more minimal dominating sets are known. For several classes of graphs, we substantially improve the upper bound on the maximum number of minimal dominating sets in graphs on

n

vertices. In some cases, we provide examples of graphs whose number of minimal dominating sets exactly matches the proved upper bound for that class, thereby showing that these bounds are tight. For all considered graph classes, the upper bound proofs are constructive and can easily be transformed into algorithms enumerating all minimal dominating sets of the input graph.

The classical group testing problem asks to determine at most

d

defective elements in a set of

n

elements, by queries to subsets that return Yes if the subset contains some defective, and No if the subset is free of defectives. By the entropy lower bound,

$\log_2\sum_{i=0}^d{n\choose i}$

tests, which is essentially

d

log

2

n

, are needed at least. We devise group testing strategies that combine two features: They achieve this optimal query bound asymptotically, with a factor 1 + 

o

(1) as

n

grows, and they work in a fixed number of stages of parallel queries. Our strategies are randomized and have a controlled failure probability, i.e., constant but arbitrarily small. We consider different settings (known or unknown

d

, probably correct or verified outcome), and we aim at the smallest possible number of stages. In particular, 2 stages are sufficient if

d

grows slowly enough with

n

, and 4 stages are sufficient if

d

 = 

o

(

n

).

Modal dependence logic (

MDL

) was introduced recently by Väänänen. It enhances the basic modal language by an operator = (·). For propositional variables

p

1

,…,

p

n

the atomic formula = (

p

1

,…,

p

n

 − 1

,

p

n

) intuitively states that the value of

p

n

is determined solely by those of

p

1

,…,

p

n

 − 1

.

We show that model checking for

MDL

formulae over Kripke structures is

NP

-complete and further consider fragments of

MDL

obtained by restricting the set of allowed propositional and modal connectives. It turns out that several fragments, e.g., the one without modalities or the one without propositional connectives, remain

NP

-complete.

We also consider the restriction of

MDL

where the length of each single dependence atom is bounded by a number that is fixed for the whole logic. We show that the model checking problem for this bounded

MDL

is still

NP

-complete. Furthermore we almost completely classifiy the computational complexity of the model checking problem for all restrictions of propositional and modal operators for both unbounded as well as bounded

MDL

.

An extended version of this article can be found on arXiv.org [3].

ACM Subject Classifiers:

F.2.2 Complexity of proof procedures; F.4.1 Modal logic; D.2.4 Model checking.

Given an

n

-tape nondeterministic finite automaton (NFA)

M

with a one-way read-only head per tape and a right end marker $ on each tape, and a nonnegative integer

k

, we say that

M

is weakly

k

-synchronized if for every

n

-tuple

x

 = (

x

1

, …,

x

n

) that is accepted, there is a computation on

x

such that at any time during the computation, no pair of input heads, neither of which is on $, are more than

k

cells apart. As usual, an

n

-tuple

x

 = (

x

1

, …,

x

n

) is accepted if

M

eventually reaches the configuration where all

n

heads are on $ in an accepting state. We show decidable and undecidable results concerning questions such as: (1) Given

M

, is it weakly

k

-synchronized for some

k

(resp., for a specified

k

) and (2) Given

M

, is there a weakly

k

-synchronized

M

′ for some

k

(resp., for a specified

k

) such that

L

(

M

′) = 

L

(

M

)? Most of our results are the strongest possible in the sense that slight restrictions on the models make the undecidable problems decidable. A few questions remain open.

Visibly Pushdown Transducers (

VPT

) form a subclass of pushdown transducers. In this paper, we investigate the extension of

VPT

with visibly pushdown look-ahead (

VPT

la

). Their transitions are guarded by visibly pushdown automata that can check whether the well-nested subword starting at the current position belongs to the language they define. First, we show that

VPT

la

are not more expressive than

VPT

, but are exponentially more succinct. Second, we show that the class of deterministic

VPT

la

corresponds exactly to the class of functional

VPT

, yielding a simple characterization of functional

VPT

. Finally, we show that while

VPT

la

are exponentially more succinct than

VPT

, checking equivalence of functional

VPT

la

is, as for

VPT

,

ExpT-C

. As a consequence, we show that any functional

VPT

is equivalent to an unambiguous one.

Spira [28] showed that any Boolean formula of size

s

can be simulated in depth

O

(log

s

). We generalize Spira’s theorem and show that any Boolean

circuit

of size

s

with segregators of size

f

(

s

) can be simulated in depth

O

(

f

(

s

)log

s

). If the segregator size is at least

s

ε

for some constant

ε

 > 0, then we can obtain a simulation of depth

O

(

f

(

s

)). This improves and generalizes a simulation of polynomial-size Boolean circuits of constant treewidth

k

in depth

O

(

k

2

log

n

) by Jansen and Sarma [17]. Since the existence of small balanced separators in a directed acyclic graph implies that the graph also has small segregators, our results also apply to circuits with small separators. Our results imply that the class of languages computed by non-uniform families of polynomial-size circuits that have constant size segregators equals non-uniform

NC

1

.

Considering space bounded Turing machines to generate the circuits, for

f

(

s

)log

2

s

-space uniform families of Boolean circuits our small-depth simulations are also

f

(

s

)log

2

s

-space uniform. As a corollary, we show that the Boolean Circuit Value problem for circuits with constant size segregators (or separators) is in deterministic

SPACE

(log

2

n

). Our results also imply that the Planar Circuit Value problem, which is known to be

P

-Complete [16], can be solved in deterministic

$SPACE (\sqrt{n} \log n)$

.

Inspired by the concept of a consistent correlation for Boolean equation systems, we introduce and study a novel relation, called

consistent consequence

. We show that it can be used as an approximation of the solution to an equation system. For the closed, simple and recursive fragment of equation systems we prove that it coincides with

direct simulation

for parity games. In addition, we show that deciding both consistent consequence and consistent correlations are coNP-complete problems, and we provide a sound and complete proof system for consistent consequence. As an application, we define a novel abstraction mechanism for parameterised Boolean equation systems and we establish its correctness using our theory.

The

k

-

Coloring

problem is to test whether a graph can be colored with at most

k

colors such that no two adjacent vertices receive the same color. If a graph

G

does not contain a graph

H

as an induced subgraph, then

G

is called

H

-free. For any fixed graph

H

on at most 6 vertices, it is known that 3-

Coloring

is polynomial-time solvable on

H

-free graphs whenever

H

is a linear forest and

NP

-complete otherwise. By solving the missing case

P

2

 + 

P

3

, we prove the same result for 4-

Coloring

provided that

H

is a fixed graph on at most 5 vertices.

Length-

q

substrings, or

q

-grams, can represent important characteristics of text data, and determining the frequencies of all

q

-grams contained in the data is an important problem with many applications in the field of data mining and machine learning. In this paper, we consider the problem of calculating the

non-overlapping frequencies

of all

q

-grams in a text given in compressed form, namely, as a straight line program (SLP). We show that the problem can be solved in

O

(

q

2

n

) time and

O

(

qn

) space where

n

is the size of the SLP. This generalizes and greatly improves previous work (Inenaga & Bannai, 2009) which solved the problem only for

q

 = 2 in

O

(

n

4

log

n

) time and

O

(

n

3

) space.

In this paper we propose an improved efficient approximation scheme for the multiple knapsack problem (MKP). Given a set

${\mathcal A}$

of

n

items and set

${\mathcal B}$

of

m

bins with possibly different capacities, the goal is to find a subset

$S \subseteq{\mathcal A}$

of maximum total profit that can be packed into

${\mathcal B}$

without exceeding the capacities of the bins. Chekuri and Khanna presented a PTAS for MKP with arbitrary capacities with running time

$n^{O(1/\epsilon^8 \log(1/\epsilon))}$

. Recently we found an efficient polynomial time approximation scheme (EPTAS) for MKP with running time

$2^{O(1/\epsilon^5 \log(1/\epsilon))} poly(n)$

. Here we present an improved EPTAS with running time

$2^{O(1/\epsilon \log^4(1/\epsilon))} + poly(n)$

. If the integrality gap between the ILP and LP objective values for bin packing with different sizes is bounded by a constant, the running time can be further improved to

$2^{O(1/\epsilon \log^2(1/\epsilon))} + poly(n)$

.

The main result of this paper is an algorithm counting maximal independent sets in graphs with maximum degree at most 3 in time

O

*

(1.2570

n

) and polynomial space.

Iterated hairpin completion is an operation on formal languages that is inspired by the hairpin formation in DNA biochemistry. Iterated hairpin completion of a word (or more precisely a singleton language) is always a context-sensitive language and for some words it is known to be non-context-free. However, it is unknown whether regularity of iterated hairpin completion of a given word is decidable. Also the question whether iterated hairpin completion of a word can be context-free but not regular was asked in literature. In this paper we investigate iterated hairpin completions of non-crossing words and, within this setting, we are able to answer both questions. For non-crossing words we prove that the regularity of iterated hairpin completions is decidable and that if iterated hairpin completion of a non-crossing word is not regular, then it is not context-free either.

The traveling salesman problem (TSP) is one of the most fundamental optimization problems. We consider the

β

-metric traveling salesman problem (Δ

β

-TSP), i.e., the TSP restricted to graphs satisfying the

β

-triangle inequality

c

({

v

,

w

}) ≤ 

β

(

c

({

v

,

u

}) + 

c

(

u

,

w

})), for some cost function

c

and any three vertices

u

,

v

,

w

. The well-known path matching Christofides algorithm (PMCA) guarantees an approximation ratio of

$\frac{3}{2}\beta^2$

and is the best known algorithm for the Δ

β

-TSP, for 1 ≤ 

β

 ≤ 2. We provide a complete analysis of the algorithm. First, we correct an error in the original implementation that may produce an invalid solution. Using a worst-case example, we then show that the algorithm cannot guarantee a better approximation ratio. The example can be reused for the PMCA variants for the Hamiltonian path problem with zero and one prespecified endpoints. For two prespecified endpoints, we cannot reuse the example, but we construct another worst-case example to show the optimality of the analysis also in this case.

It is well known that for each context-free language there exists a regular language with the same Parikh image. We investigate this result from a descriptional complexity point of view, by proving tight bounds for the size of deterministic automata accepting regular languages Parikh equivalent to some kinds of context-free languages. First, we prove that for each context-free grammar in Chomsky normal form with a fixed terminal alphabet and

h

variables, generating a bounded language

L

, there exists a deterministic automaton with at most

$2^{h^{O(1)}}$

states accepting a regular language Parikh equivalent to

L

. This bound, which generalizes a previous result for languages defined over a one letter alphabet, is optimal. Subsequently, we consider the case of arbitrary context-free languages defined over a two letter alphabet. Even in this case we are able to obtain a similar bound. For alphabets of at least three letters the best known upper bound is a double exponential in

h

.

We consider the problem of computing all-pairs shortest paths in a directed graph with non-negative real weights assigned to vertices.

For an

n

×

n

0 − 1 matrix

C

, let

K

C

be the complete weighted graph on the rows of

C

where the weight of an edge between two rows is equal to their Hamming distance. Let

MWT

(

C

) be the weight of a minimum weight spanning tree of

K

C

.

We show that the all-pairs shortest path problem for a directed graph

G

on

n

vertices with non-negative real weights and adjacency matrix

A

G

can be solved by a combinatorial randomized algorithm in time

$$\widetilde{O}(n^{2}\sqrt{n + \min\{MWT(A_G), MWT(A_G^t)\}})$$

As a corollary, we conclude that the transitive closure of a directed graph

G

can be computed by a combinatorial randomized algorithm in the aforementioned time.

We also conclude that the all-pairs shortest path problem for vertex-weighted uniform disk graphs induced by point sets of bounded density within a unit square can be solved in time

$\widetilde{O}(n^{2.75})$

.

We survey some work concerned with small universal Turing machines, cellular automata, tag systems, and other simple models of computation. For example it has been an open question for some time as to whether the smallest known universal Turing machines of Minsky, Rogozhin, Baiocchi and Kudlek are efficient (polynomial time) simulators of Turing machines. These are some of the most intuitively simple computational devices and previously the best known simulations were exponentially slow. We discuss recent work that shows that these machines are indeed efficient simulators. In addition, another related result shows that Rule 110, a well-known elementary cellular automaton, is efficiently universal. We also discuss some old and new universal program size results, including the smallest known universal Turing machines. We finish the survey with results on generalised and restricted Turing machine models including machines with a periodic background on the tape (instead of a blank symbol), multiple tapes, multiple dimensions, and machines that never write to their tape. We then discuss some ideas for future work.

We characterize the hitting sets for read-once branching programs of width 3 by a so-called richness condition which is independent of a rather technical definition of branching programs. The richness property proves to be (in certain sense) necessary and sufficient condition for such hitting sets. In particular, we show that any rich set extended with all strings within Hamming distance of 3 is a hitting set for width-3 read-once branching programs. Applying this result to an example of an efficiently constructible rich set from our previous work we achieve an explicit polynomial time construction of an

ε

-hitting set for read-once branching programs of width 3 with acceptance probability

ε

 > 11/12.

The main purpose of this paper is to prove that (promise) problem

Quantum State Identicalness

(abbreviated

QSI

) is

essentially

complete for perfect zero-knowledge quantum interactive proof (

QPZK

). Loosely speaking, problem

QSI

is to decide whether two efficiently preparable quantum states (captured by quantum circuit of polynomial size) are identical or far apart (in trace distance). It is worthy noting that our result does not have classical counterpart yet; natural complete problem for perfect zero-knowledge interactive proof (

PZK

) is still unknown. Our proof generalizes Watrous’ completeness proof for statistical zero-knowledge quantum interactive proof (

QSZK

), with an extra idea inspired by Malka to deal with completeness error. With complete problem at our disposal, we can immediately prove (and reprove) several interesting facts about

QPZK

.

In probabilistic game structures, probabilistic alternating simulation (PA-simulation) relations preserve formulas defined in probabilistic alternating-time temporal logic with respect to the behaviour of a subset of players. We propose a partition based algorithm for computing the largest PA-simulation. It is to our knowledge the first such algorithm that works in polynomial time. Our solution extends the generalised coarsest partition problem (GCPP) to a game-based setting with mixed strategies. The algorithm has higher complexities than those in the literature for non-probabilistic simulation and probabilistic simulation without mixed actions, but slightly improves the existing result for computing probabilistic simulation with respect to mixed actions.

The traditional client/server architecture for web service delivery fails to naturally scale. This results in growing costs to the service provider for powerful hardware or extensive use of Content Distribution Networks. A P2P overlay network provides inherent scalability with multiple benefits to both clients and servers. In this paper, we provide analysis, design and prototype implementation of Cooperative Web Cache, which allows us to scale web service delivery and cope with demand spikes by employing clients in content replication. To demonstrate performance capabilities, we provide a prototype emulation for both client and server.

In our work we present an approach to the Named Entity Disambiguation based on semantic similarity measure. We employ existing explicit semantics present in datasets such as Wikipedia to construct a disambiguation dictionary and vector–based word model. The analysed documents are transformed into semantic vectors using explicit semantic analysis. The relatedness is computed as cosine similarity between the vectors. The experimental evaluation shows that the proposed approach outperforms traditional approaches such as latent semantic analysis.

Nowadays there exist many approaches to support design pattern instantiation, evolution, etc., but most of the approaches focus mainly at the design level (i.e. model). By the transition to the source code level the pattern instances become almost invisible in the huge amount of source code lines. The goal of this paper is to present our method supporting design pattern instantiation, evolution and identification in the source code. The method is based on source code annotations and feature models of individual patterns. The method does not require a manual annotation of the source code by a human, instead the method works on the idea of architectural and design information propagation and expansion from higher levels of abstraction (i.e. models) into the source code. In this paper we also present a method defining how to connect the necessary knowledge to the model and the source code.

Formal description techniques, such as

Lotos

and

Sdl

, have been proven as a successful means for developing communication protocols and distributed systems. Meanwhile the Unified Modeling Language (UML) has achieved wide acceptance. It is, however, less applied in the field of protocol design due to the lack of an appropriate formal semantics. In this paper we propose a formalization technique for UML activity diagrams using the compositional Temporal Logic of Actions (cTLA). We use cTLA because it can express correctness properties in temporal logic and can also be verified formally using several model checking mechanisms. The approach consists of two steps. First, we predefine the formal semantics of the most commonly used UML activity nodes using simple cTLA. In the second step we derive the

functional semantics

of the activity diagram by mapping it to a compositional cTLA process. We illustrate our approach for a connection set up as an example. Finally we present with the

Activity to cTLA generator

a tool to automate this process.

Model transformation languages have been mainly used by researchers – the software engineering industry has not yet widely accepted the model driven software development (MDSD). One of the main reasons is the complexity of metamodelling principles the developers are required to know to actually use model transformations in the way the OMG has stated. We offer the basic principles how to create domain-specific model transformation languages which can be used by developers relying only on familiar modelling concepts. We propose to use simple graphical mappings to specify the correspondence between source and target models which are represented using trees based on the concrete syntax of underlying modelling languages. If such principles were followed, then the range of potential users of model transformation languages would increase significantly.

Service resilience, defined as the continued availability of a service despite failures and other negative changes in its environment, is vital in many systems. It is typically achieved by state machine replication using group communication middleware for coordination of service replicas. In this paper we focus on systems that represent critical data as Web resources identified by Uniform Resource Identifiers (URIs). The best examples of such systems are RESTful web services. We present

RESTGroups

: a group communication

front-end

for RESTful web services. Our system is based on Spread – a popular group communication toolkit. Contrary to Spread and other such toolkits, we represent group communication services as resources on the Web, addressed by URIs. In the paper, we describe the system architecture and the API.

In order to compute page rankings, search algorithms primarily utilize information related to page content and link structure. Microblog as a phenomenon of today provides additional, potentially relevant, information – short messages often containing hypertext links to web resources. Such source is particularly valuable when considering a temporal aspect of information, which is being published every second. In this paper we present a method for resource ranking based on Twitter data structure processing. We apply various graph algorithms leveraging the notion of a node centrality in order to deduce microblog-based resource ranking. Our method ranks a microblog user based on his followers count with respect to a number of (re)posts and reflects it into resource ranking. The evaluation of the method showed that micro-based resource ranking

a

) can not be substituted by a common form of an explicit user rating, and

b

) has the great potential for search improvement.

Social networks, their increasing popularity reaching hundreds of million users, demand advance software architecture. Countless requests per second necessitate flexible and utmost efficiency and high performance. This article is focused on development of such a web-based service offering social functionality to end users, but from the technology point of view represents state-of-the-art in current usage of the latest technologies. Those technologies mentioned further are often used for the first time in such a complex project. High volume data distribution is handled by Apache Hadoop framework together with Hadoop Distributed File System (HDFS) and MapReduce. Therewithal, non-relational distributed database HBase and Memcached tool ensures scalability and high throughput helping with often accessed information. Inner architecture of the social subsystem has been implemented within three-layer structure (services/data access/transmission). Social subsystem among others deals with one-way (unsymmetrical) relationship generation or cancellation between users but events either. Particular system entities are allowed to add comments, follow or “like” others. In the end, testing phase, deployment and practical utilization (although the resulted solution is completely independent) is demonstrated on practical example of case study

Takeplace

– complex tool for event management.

Currently, testing is still the most important approach to reduce the amount of software defects. Software quality metrics help to prioritize where additional testing is necessary by measuring the quality of the code. Most approaches to estimate whether some unit of code is sufficiently tested are based on code coverage, which measures what code fragments are exercised by the test suite. Unfortunately, code coverage does not measure to what extent the test suite checks the intended functionality.

We propose

state coverage

, a metric that measures the ratio of state updates that are read by assertions with respect to the total number of state updates, and we present efficient algorithms to measure state coverage. Like code coverage, state coverage is simple to understand and we show that it is effective to measure and easy to aggregate. During a preliminary evaluation on several open-source libraries, state coverage helped to identify multiple unchecked properties and detect several bugs.

Component-interaction automata is a verification oriented formalism devised to be general enough to capture important aspects of component interaction in various kinds of component systems. A factorization problem naturally arises in formalisms that are based on composition. In general, the factorization problem may be presented as finding a solution

X

to the equation

M

|

X

 ≃ 

S

, where | is a composition and ≃ a behavioural equivalence. In our framework, the equivalence is the weak bisimulation and composition is parametrized. We provide a solution for the factorization problem which is built on top of the approach of Qin and Lewis [13].

We consider documents with restricted access rights, where some

segments

of the document are encrypted in order to prevent unauthorized reading. The access rights to such a document are described by an

access graph

. It is a directed acyclic graph; each node describing a different access rights level. It is assumed that a user having the rights corresponding to a node

v

has also all rights corresponding to all nodes

w

such that there is a directed path from

v

to

w

in the access graph. Then, to each node

v

we assign a key

K

v

and use this key to encrypt the segment of the document corresponding to the access level

v

.

We consider key management schemes and encoding auxiliary information in the document which ensure that a user who gets a single key corresponding to his access level

v

can derive all keys

K

w

for

w

 = 

v

or

w

being an ancestor of

v

in the access graph.

In this paper we show how to minimize the total size of auxiliary keying information stored in the document. We provide an algorithm based on node disjoint paths in the access graph and key derivation based on one-way functions. We show that the algorithm chooses the paths in an optimal way.

We present an information-flow type system for a distributed object-oriented language with active objects, asynchronous method calls and futures. The variables of the program are classified as high and low. We allow

while

cycles with high guards to be used but only if they are not followed (directly or through synchronization) by an assignment to a low variable. To ensure the security of synchronization, we use a high and a low lock for each concurrent object group (cog). In some cases, we must allow a high lock held by one task to be overtaken by another, if the former is about to make a low side effect but the latter cannot make any low side effects. This is necessary to prevent synchronization depending on high variables from influencing the order of low side effects in different cogs. We prove a non-interference result for our type system.

This paper proposes a new approach for enhancing the robustness of wavelet-based image watermarking algorithms. The method adjusts wavelet used in the process of image watermarking in order to maximize resistance against image processing operations. Effectiveness of the approach is demonstrated using blind multiplicative watermarking algorithm, but it can easily be generalized to all wavelet-based watermarking algorithms. Presented results demonstrate that wavelets generated using proposed approach outperform other wavelet bases commonly used in image watermarking in terms of robustness to removal attacks.

The paper presents a performance prediction and optimisation tool MAK€that allows users to model enterprises in a visually rich and intuitive way. The tool automatically generates a scheduling model describing all choices that users can do when optimising production. This model then goes to the Optimiser Module that generates schedules optimising on-time-in-full performance criterion while meeting the constraints of the firm and the customer demand. Finally, the Performance Manager Module shows the decision maker what is the best possible outcome for the firm given the inputs from the Enterprise Modeller. The Optimiser Module, which is the main topic of this paper, is implemented using constraint-based solving techniques with specific search heuristics for this type of problems. It demonstrates practical applicability of constraint-based scheduling – one of the killer application areas of constraint programming, a technology originated from AI research.

When we encode constraints as Boolean formulas, a natural question is whether the encoding ensures a “propagation completeness” property: is the basic unit propagation mechanism able to deduce all the literals that are logically valid? We consider the problem of automatically finding encodings with this property. Our goal is to compile a naïve definition of a constraint into a good, propagation-complete encoding. Well-known Knowledge Compilation techniques from AI can be used for this purpose, but the constraints for which they can produce a polynomial size encoding are few. We show that the notion of

empowerment

recently introduced in the SAT literature allows producing encodings that are shorter than with previous techniques, sometimes exponentially.

In this paper, we deal with an enhanced problem of cost-sensitive classification, where not only the cost of misclassification needs to be minimized, but also the total cost of tests and their requirements. To solve this problem, we propose a novel method CS-UID based on the theory of Unconstrained Influence Diagrams (UIDs). We empirically evaluate and compare CS-UID with an existing algorithm for test-cost sensitive classification (TCSNB) on multiple real-world public referential datasets. We show that CS-UID outperforms TCSNB.

Artificial intelligence and data mining techniques offer a chance to make education tailored to every student. One of possible contributions of automated techniques is a selection of suitable problems for individual students based on previously collected data. To achieve this goal, we propose a model of problem solving times, which predicts how much time will a particular student need to solve a given problem. Our model is an analogy of the models used in the item response theory, but instead of probability of a correct answer, we model problem solving time. We also introduce a web-based problem solving tutor, which uses the model to make adaptive predictions and recommends problems of suitable difficulty. The system already collected extensive data on human problem solving. Using this dataset we evaluate the model and discuss an insight gained by an analysis of model parameters.

General Game Playing (GGP) is a specially designed environment for creating and testing competitive agents which can play variety of games. The fundamental motivation is to advance the development of various artificial intelligence methods operating together in a previously unknown environment. This approach extrapolates better on real world problems and follows artificial intelligence paradigms better than dedicated single-game optimized solutions. This paper presents a universal method of constructing the heuristic evaluation function for any game playable within the GGP framework. The algorithm embraces distinctive discovery of candidate features to be included in the evaluation function and learning their correlations with actions performed by the players and the game score. Our method integrates well with the UCT algorithm which is currently the state-of-the-art approach in GGP.

From automotive and up to telecommunication industry, configuration and simulation are used for solving complex problems connected to the ever growing number of components, which have to work together. To assist these needs, many tools are nowadays available. Modeling languages like Matlab/Simulink or Modelica are often used to model the dependencies between the components of physical systems. However these are less suitable for the area of knowledge-based systems. In this paper, we present a modeling language, which combines the two different directions. SiMoL is an object-oriented language that allows representing systems comprising basic and hierarchical components. We state the syntax and the semantics of the language, referring also to the implementation of SiMoL, which is based on the MINION constraint solver. Furthermore, we discuss how the obtained model can be used for simulation and re-configuration.