Skip to main content
Top

2015 | Book

Mathematical Foundations of Computer Science 2015

40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I

Editors: Giuseppe F Italiano, Giovanni Pighizzini, Donald T. Sannella

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

insite
SEARCH

About this book

This two volume set LNCS 9234 and 9235 constitutes the refereed conference proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015, held in Milan, Italy, in August 2015. The 82 revised full papers presented together with 5 invited talks were carefully selected from 201 submissions. The papers feature high-quality research in all branches of theoretical computer science. They have been organized in the following topical main sections: logic, semantics, automata, and theory of programming (volume 1) and algorithms, complexity, and games (volume 2).

Table of Contents

Frontmatter

Invited Contributions

Frontmatter
Minimal and Monotone Minimal Perfect Hash Functions

A minimal perfect hash function (MPHF) is a (data structure providing a) bijective map from a set

S

of

n

keys to the set of the first

n

natural numbers. In the static case (i.e., when the set

S

is known in advance), there is a wide spectrum of solutions available, offering different trade-offs in terms of construction time, access time and size of the data structure. MPHFs have been shown to be useful to compress data in several data management tasks. In particular,

order-preserving

minimal perfect hash functions have been used to retrieve the position of a key in a given list of keys: however, the ability to preserve any given order leads to an unavoidable

$$\varOmega (n \log n)$$

Ω

(

n

log

n

)

lower bound on the number of bits required to store the function. Recently, it was observed that very frequently the keys to be hashed are sorted in their intrinsic (i.e., lexicographical) order. This is typically the case of dictionaries of search engines, list of URLs of web graphs, etc. MPHFs that preserve the intrinsic order of the keys are called

monotone

(MMPHF). The problem of building MMPHFs is more recent and less studied (for example, no lower bounds are known) but once more there is a wide spectrum of solutions available, by now. In this paper, we survey some of the most practical techniques and tools for the construction of MPHFs and MMPHFs.

Paolo Boldi
Equational Properties of Fixed Point Operations in Cartesian Categories: An Overview

Several fixed point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed point operation and binary supremum, but not involving residuals.

Zoltán Ésik
Reversible and Irreversible Computations of Deterministic Finite-State Devices

Finite-state devices with a read-only input tape that may be equipped with further resources as queues or pushdown stores are considered towards their ability to perform reversible computations. Some aspects of the notion of logical reversibility are addressed. We present some selected results on the decidability, uniqueness, and size of minimal reversible deterministic finite automata. The relations and properties of reversible automata that are equipped with storages are discussed, where we exemplarily stick with the storage types queue and pushdown store. In particular, the computational capacities, decidability problems, and closure properties are the main topics covered, and we draw attention to the overall picture and some of the main ideas involved.

Martin Kutrib
Robust Inference and Local Algorithms

We introduce a new feature to inference and learning which we call

robustness

. By robustness we intuitively model the case that the observation of the learner might be corrupted. We survey a new and novel approach to model such possible corruption as a zero-sum game between an adversary that selects the corruption and a leaner that predict the correct label. The corruption of the observations is done in a worse-case setting, by an adversary, where the main restriction is that the adversary is limited to use one of a fixed know class of modification functions. The main focus in this line of research is on

efficient

algorithms both for the inference setting and for the learning setting. In order to be efficient in the dimension of the domain, one cannot hope to inspect all the possible inputs. For this, we have to invoke local computation algorithms, that inspect only a logarithmic fraction of the domain per query.

Yishay Mansour

Logic, Semantics, Automata and Theory of Programming

Frontmatter
Uniform Generation in Trace Monoids

We consider the problem of random uniform generation of traces (the elements of a free partially commutative monoid) in light of the uniform measure on the boundary at infinity of the associated monoid. We obtain a product decomposition of the uniform measure at infinity if the trace monoid has several irreducible components—a case where other notions such as Parry measures, are not defined. Random generation algorithms are then examined.

Samy Abbes, Jean Mairesse
When Are Prime Formulae Characteristic?

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek’s branching-time spectrum.

L. Aceto, D. Della Monica, I. Fábregas, A. Ingólfsdóttir
Stochastization of Weighted Automata

Nondeterministic weighted finite automata

(WFAs) map input words to real numbers. Each transition of a WFA is labeled by both a letter from some alphabet and a weight. The weight of a run is the sum of the weights on the transitions it traverses, and the weight of a word is the minimal weight of a run on it. In

probabilistic weighted automata

(PWFAs), the transitions are further labeled by probabilities, and the weight of a word is the expected weight of a run on it. We define and study

stochastization

of WFAs: given a WFA

$$\mathcal{A}$$

A

, stochastization turns it into a PWFA

$$\mathcal{A}'$$

A

by labeling its transitions by probabilities. The weight of a word in

$$\mathcal{A}'$$

A

can only increase with respect to its weight in

$$\mathcal{A}$$

A

, and we seek stochastizations in which

$$\mathcal{A}'$$

A

$$\alpha $$

α

-approximates

$$\mathcal{A}$$

A

for the minimal possible factor

$$\alpha \ge 1$$

α

1

. That is, the weight of every word in

$$\mathcal{A}'$$

A

is at most

$$\alpha $$

α

times its weight in

$$\mathcal{A}$$

A

. We show that stochastization is useful in reasoning about the competitive ratio of randomized online algorithms and in approximated determinization of WFAs. We study the problem of deciding, given a WFA

$$\mathcal{A}$$

A

and a factor

$$\alpha \ge 1$$

α

1

, whether there is a stochastization of

$$\mathcal{A}$$

A

that achieves an

$$\alpha $$

α

-approximation. We show that the problem is in general undecidable, yet can be solved in PSPACE for a useful class of WFAs.

Guy Avni, Orna Kupferman
Algebraic Synchronization Criterion and Computing Reset Words

We refine results about relations between Markov chains and synchronizing automata. We express the condition that an automaton is synchronizing in terms of linear algebra, and obtain upper bounds for the reset thresholds of automata with a short word of a small rank. The results are applied to make several improvements in the area.

We improve the best general upper bound for reset thresholds of finite prefix codes (Huffman codes): we show that an

n

-state synchronizing decoder has a reset word of length at most

$$O(n \log ^3 n)$$

O

(

n

log

3

n

)

. Also, we prove the Černý conjecture for

n

-state automata with a letter of rank at most

$$\root 3 \of {6n-6}$$

6

n

-

6

3

. In another corollary, based on the recent results of Nicaud, we show that the probability that the Černý conjecture does not hold for a random synchronizing binary automaton is exponentially small in terms of the number of states. It follows that the expected value of the reset threshold of an

n

-state random synchronizing binary automaton is at most

$$n^{7/4+o(1)}$$

n

7

/

4

+

o

(

1

)

.

Moreover, reset words of the lengths within our bounds are computable in polynomial time. We present suitable algorithms for this task for various classes of automata for which our results can be applied. These include (quasi-)one-cluster and (quasi-)Eulerian automata.

Mikhail Berlinkov, Marek Szykuła
Recurrence Function on Sturmian Words: A Probabilistic Study

This paper is a first attempt to describe the probabilistic behaviour of a random Sturmian word. It performs the probabilistic analysis of the recurrence function which provides precise information on the structure of such a word. With each Sturmian word of slope

$$\alpha $$

α

, we associate particular sequences of factor lengths which have a given “position” with respect to the sequence of continuants of

$$\alpha $$

α

, we then let

$$\alpha $$

α

to be uniformly drawn inside the unit interval [0,1]. This probabilistic model is well-adapted to better understand the role of the position in the recurrence properties.

Valérie Berthé, Eda Cesaratto, Pablo Rotondo, Brigitte Vallée, Alfredo Viola
Exponential-Size Model Property for PDL with Separating Parallel Composition

Propositional dynamic logic is extended with a parallel program having a separating semantic: the program

$$(\alpha \parallel \beta )$$

(

α

β

)

executes

$$\alpha $$

α

and

$$\beta $$

β

on two substates of the current state. We prove that when the composition of two substates is deterministic, the logic has the exponential-size model property. The proof is by a piecewise filtration using an adaptation of the Fischer-Ladner closure. We conclude that the satisfiability of the logic is decidable in NEXPTIME.

Joseph Boudou
A Circuit Complexity Approach to Transductions

Low circuit complexity classes and regular languages exhibit very tight interactions that shade light on their respective expressiveness. We propose to study these interactions at a functional level, by investigating the deterministic rational transductions computable by constant-depth, polysize circuits. To this end, a circuit framework of independent interest that allows variable output length is introduced. Relying on it, there is a general characterization of the set of transductions realizable by circuits. It is then decidable whether a transduction is definable in

$$\mathrm{AC}^0$$

AC

0

and, assuming a well-established conjecture, the same for

$$\mathrm{ACC}^0$$

ACC

0

.

Michaël Cadilhac, Andreas Krebs, Michael Ludwig, Charles Paperman
Locally Chain-Parsable Languages

If a context-free language enjoys the local parsability property then, no matter how the source string is segmented, each segment can be parsed independently, and an efficient parallel parsing algorithm becomes possible. The new class of locally chain-parsable languages (LCPL), included in deterministic context-free languages, is here defined by means of the chain-driven automaton and characterized by decidable properties of grammar derivations. Such automaton decides to reduce or not a factor in a way purely driven by the terminal characters, thus extending the well-known concept of Input-Driven (ID) (visibly) pushdown machines. LCPL extend and improve the practically relevant operator-precedence languages (Floyd), which are known to strictly include the ID languages, and for which a parallel-parser generator exists. Consistently with the classical results for ID, chain-compatible LCPL are closed under reversal and Boolean operations, and language inclusion is decidable.

Stefano Crespi Reghizzi, Violetta Lonati, Dino Mandrioli, Matteo Pradella
Classes of Languages Generated by the Kleene Star of a Word

In this paper, we study the lattice and the Boolean algebra, possibly closed under quotient, generated by the languages of the form

$$u^*$$

u

, where

u

is a word. We provide effective equational characterisations of these classes, i.e. one can decide using our descriptions whether a given regular language belongs or not to each of them.

Laure Daviaud, Charles Paperman
Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus

We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus w.r.t.

MSO

, when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of

MSO

and the mu-calculus:

MSO

with path relation

and the

jumping mu-calculus

. While “bounded-memory” binary relations bring about no extra expressivity to either of the two logics, “unbounded-memory” binary relations make the bisimulation-invariant fragment of

MSO

with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfect-information inhabits the gap.

Cătălin Dima, Bastien Maubert, Sophie Pinchinat
Weighted Automata and Logics on Graphs

Weighted automata model quantitative features of the behavior of systems and have been investigated for various structures like words, trees, traces, pictures, and nested words. In this paper, we introduce a general model of weighted automata acting on graphs, which form a quantitative version of Thomas’ unweighted model of graph acceptors. We derive a Nivat theorem for weighted graph automata which shows that their behaviors are precisely those obtainable from very particular weighted graph automata and unweighted graph acceptors with a few simple operations. We also show that a suitable weighted MSO logic is expressively equivalent to weighted graph automata. As a consequence, we obtain corresponding Büchi-type equivalence results known from the recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words. Establishing such a general result has been an open problem for weighted logic for some time.

Manfred Droste, Stefan Dück
Longest Gapped Repeats and Palindromes

A gapped repeat (respectively, palindrome) occurring in a word

w

is a factor

uvu

(respectively,

$$u^Rvu$$

u

R

v

u

) of

w

. We show how to compute efficiently, for every position

i

of the word

w

, the longest prefix

u

of

w

[

i

..

n

] such that

uv

(respectively,

$$u^Rv$$

u

R

v

) is a suffix of

$$w[1..i-1]$$

w

[

1

.

.

i

-

1

]

(defining thus a gapped repeat

uvu

– respectively, palindrome

$$u^Rvu$$

u

R

v

u

), and the length of

v

is subject to various types of restrictions.

Marius Dumitran, Florin Manea
Quasiperiodicity and Non-computability in Tilings

We study tilings of the plane that combine strong properties of different nature: combinatorial and algorithmic. We prove the existence of a tile set that accepts only quasiperiodic and non-recursive tilings. Our construction is based on the fixed point construction [

12

]; we improve this general technique and make it enforce the property of local regularity of tilings needed for quasiperiodicity. We prove also a stronger result: any

$$\mathrm \Pi _1^0$$

Π

1

0

-class can be recursively transformed into a tile set so that the Turing degrees of the resulting tilings consists exactly of the upper cone based on the Turing degrees of the latter.

Bruno Durand, Andrei Romashchenko
The Transitivity Problem of Turing Machines

A Turing machine is topologically transitive if every partial configuration — that is a state, a head position, plus a finite portion of the tape — can reach any other partial configuration, provided that they are completed into proper configurations. We study topological transitivity in the dynamical system models of Turing machines with moving head, moving tape and for the trace-shift and we prove its undecidability. We further study minimality, the property of every configuration reaching every partial configuration.

Anahí Gajardo, Nicolas Ollinger, Rodrigo Torres-Avilés
Strong Inapproximability of the Shortest Reset Word

The Černý conjecture states that every

n

-state synchronizing automaton has a reset word of length at most

$$(n-1)^2$$

(

n

-

1

)

2

. We study the hardness of finding short reset words. It is known that the exact version of the problem, i.e., finding the shortest reset word, is

$$\mathrm {NP}$$

NP

-hard and

$$\mathrm {coNP}$$

coNP

-hard, and complete for the

$$\mathrm {DP}$$

DP

class, and that approximating the length of the shortest reset word within a factor of

$$O(\log n)$$

O

(

log

n

)

is

$$\mathrm {NP}$$

NP

-hard [Gerbush and Heeringa, CIAA’10], even for the binary alphabet [Berlinkov, DLT’13]. We significantly improve on these results by showing that, for every

$$\varepsilon >0$$

ε

>

0

, it is

$$\mathrm {NP}$$

NP

-hard to approximate the length of the shortest reset word within a factor of

$$n^{1-\varepsilon }$$

n

1

-

ε

. This is essentially tight since a simple

O

(

n

)-approximation algorithm exists.

Paweł Gawrychowski, Damian Straszak
Finitary Semantics of Linear Logic and Higher-Order Model-Checking

In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the

$$\lambda \,Y$$

λ

Y

-calculus formulated in a companion paper, and to replace it by a finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme

$$\mathcal {G}$$

G

, the finiteness of its interpretation in the resulting model enables us to associate to any MSO formula

$$\varphi $$

φ

a higher-order recursion scheme

$$\mathcal {G}_{\varphi }$$

G

φ

resolving the selection problem.

Charles Grellois, Paul-André Melliès
Complexity of Propositional Independence and Inclusion Logic

We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence and inclusion logic and their extensions by the classical negation.

Miika Hannula, Juha Kontinen, Jonni Virtema, Heribert Vollmer
Modal Inclusion Logic: Being Lax is Simpler than Being Strict

We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for strict and another one for lax semantics. The complexity of the lax version turns out to be complete for

EXPTIME

, whereas with strict semantics, the problem becomes

$${\mathsf{{NEXPTIME}}}$$

NEXPTIME

-complete.

Lauri Hella, Antti Kuusisto, Arne Meier, Heribert Vollmer
Differential Bisimulation for a Markovian Process Algebra

Formal languages with semantics based on ordinary differential equations (ODEs) have emerged as a useful tool to reason about large-scale distributed systems. We present

differential bisimulation

, a behavioral equivalence developed as the ODE counterpart of bisimulations for languages with probabilistic or stochastic semantics. We study it in the context of a Markovian process algebra. Similarly to Markovian bisimulations yielding an aggregated Markov process in the sense of the theory of lumpability, differential bisimulation yields a partition of the ODEs underlying a process algebra term, whereby the sum of the ODE solutions of the same partition block is equal to the solution of a single (lumped) ODE. Differential bisimulation is defined in terms of two symmetries that can be verified only using syntactic checks. This enables the adaptation to a continuous-state semantics of proof techniques and algorithms for finite, discrete-state, labeled transition systems. For instance, we readily obtain a result of compositionality, and provide an efficient partition-refinement algorithm to compute the coarsest ODE aggregation of a model according to differential bisimulation.

Giulio Iacobelli, Mirco Tribastone, Andrea Vandin
On the Hardness of Almost–Sure Termination

This paper considers the computational hardness of computing expected outcomes and deciding (universal) (positive) almost–sure termination of probabilistic programs. It is shown that computing lower and upper bounds of expected outcomes is

$$\varSigma _1^0$$

Σ

1

0

– and

$$\varSigma _2^0$$

Σ

2

0

–complete, respectively. Deciding (universal) almost–sure termination as well as deciding whether the expected outcome of a program equals a given rational value is shown to be

$$\varPi ^0_2$$

Π

2

0

–complete. Finally, it is shown that deciding (universal) positive almost–sure termination is

$$\varSigma _2^0$$

Σ

2

0

–complete (

$$\varPi _3^0$$

Π

3

0

–complete).

Benjamin Lucien Kaminski, Joost-Pieter Katoen
Graphs Identified by Logics with Counting

We classify graphs and, more generally, finite relational structures that are identified by

$${C^{2}}$$

C

2

, that is, two-variable first-order logic with counting. Using this classification, we show that it can be decided in almost linear time whether a structure is identified by

$${C^{2}}$$

C

2

. Our classification implies that for every graph identified by this logic, all vertex-colored versions of it are also identified. A similar statement is true for finite relational structures.

We provide constructions that solve the inversion problem for finite structures in linear time. This problem has previously been shown to be polynomial time solvable by Martin Otto. For graphs, we conclude that every

$${C^{2}}$$

C

2

-equivalence class contains a graph whose orbits are exactly the classes of the

$${C^{2}}$$

C

2

-partition of its vertex set and which has a single automorphism witnessing this fact.

For general

k

, we show that such statements are not true by providing examples of graphs of size linear in

k

which are identified by

$${C^{3}}$$

C

3

but for which the orbit partition is strictly finer than the

$$C^k$$

C

k

-partition. We also provide identified graphs which have vertex-colored versions that are not identified by

$$C^k$$

C

k

.

Sandra Kiefer, Pascal Schweitzer, Erkal Selman
Synchronizing Automata with Extremal Properties

We present a few classes of synchronizing automata exhibiting certain extremal properties with regard to synchronization. The first is a series of automata with subsets whose shortest extending words are of length

$$\varTheta (n^2)$$

Θ

(

n

2

)

, where

n

is the number of states of the automaton. This disproves a conjecture that every subset in a strongly connected synchronizing automaton is

cn

-extendable, for some constant

c

, and in particular, shows that the cubic upper bound on the length of the shortest reset words cannot be improved generally by means of the extension method. A detailed analysis shows that the automata in the series have subsets that require words as long as

$$n^2/4+O(n)$$

n

2

/

4

+

O

(

n

)

in order to be extended by at least one element.

We also discuss possible relaxations of the conjecture, and propose the image-extension conjecture, which would lead to a quadratic upper bound on the length of the shortest reset words. In this regard we present another class of automata, which turn out to be counterexamples to a key claim in a recent attempt to improve the Pin-Frankl bound for reset words.

Finally, we present two new series of slowly irreducibly synchronizing automata over a ternary alphabet, whose lengths of the shortest reset words are

$$n^2-3n+3$$

n

2

-

3

n

+

3

and

$$n^2-3n+2$$

n

2

-

3

n

+

2

, respectively. These are the first examples of such series of automata for alphabets of size larger than two.

Andrzej Kisielewicz, Marek Szykuła
Ratio and Weight Quantiles

Several types of weighted-automata models and formalisms to specify and verify constraints on accumulated weights have been studied in the past. The lack of monotonicity for weight functions with positive and negative values as well as for ratios of the accumulated values of non-negative weight functions renders many verification problems to be undecidable or computationally hard. Our contribution comprises polynomial-time algorithms for computing ratio and weight quantiles in Markov chains, which provide optimal bounds guaranteed almost surely or with positive probability on, e.g., cost-utility ratios or the energy conversion efficiency.

Daniel Krähmann, Jana Schubert, Christel Baier, Clemens Dubslaff
Precise Upper and Lower Bounds for the Monotone Constraint Satisfaction Problem

The

monotone constraint satisfaction problem

(MCSP) is the problem of, given an existentially quantified positive formula, decide whether this formula has a model. This problem is a natural generalization of the constraint satisfaction problem, which can be seen as the problem of determining whether a conjunctive formula has a model. In this paper we study the worst-case time complexity, measured with respect to the number of variables,

n

, of the MCSP problem parameterized by a constraint language

$$\varGamma $$

Γ

(MCSP

$$(\varGamma )$$

(

Γ

)

). We prove that the complexity of the NP-complete MCSP

$$(\varGamma )$$

(

Γ

)

problems on a given finite domain

D

falls into exactly

$$|D| - 1$$

|

D

|

-

1

cases and ranges from

$$O(2^{n})$$

O

(

2

n

)

to

$$O(|D|^n)$$

O

(

|

D

|

n

)

. We give strong lower bounds and prove that MCSP

$$(\varGamma )$$

(

Γ

)

, for any constraint language

$$\varGamma $$

Γ

over any finite domain, is solvable in

$$O(|D'|^n)$$

O

(

|

D

|

n

)

time, where

$$D'$$

D

is the domain of the core of

$$\varGamma $$

Γ

, but not solvable in

$$O(|D'|^{\delta n})$$

O

(

|

D

|

δ

n

)

time for any

$$\delta < 1$$

δ

<

1

, unless the strong exponential-time hypothesis fails. Hence, we obtain a complete understanding of the worst-case time complexity of MCSP

$$(\varGamma )$$

(

Γ

)

for constraint languages over arbitrary finite domains.

Victor Lagerkvist
Definability by Weakly Deterministic Regular Expressions with Counters is Decidable

We show that weakly deterministic regular expressions with counters (

WDRE

s) —as they are used in XML Schema— are at most exponentially larger than equivalent

DFA

s. As a consequence, the problem, whether a given

DFA

is equivalent to any

WDRE

, is decidable in

EXPSPACE

.

Markus Latte, Matthias Niewerth
On the Complexity of Reconfiguration in Systems with Legacy Components

In previous works we have proved that component reconfiguration in the presence of conflicts among components is non-primitive recursive, while it becomes poly-time if there are no conflicts and under the assumption that there are no components in the initial configuration. The case with non-empty initial configurations was left as an open problem, that we close in this paper by showing that, if there are legacy components that cannot be generated from scratch, the problem turns out to be PSpace-complete.

Jacopo Mauro, Gianluigi Zavattaro
Eliminating Recursion from Monadic Datalog Programs on Trees

We study the problem of eliminating recursion from monadic datalog programs on trees with labels taken from an infinite alphabet. We show that the boundedness problem, i.e., determining whether a datalog program is equivalent to

some

nonrecursive one is undecidable but the decidability is regained if the descendant relation is disallowed. Under similar restrictions we obtain decidability of the problem of equivalence to a

given

nonrecursive program. We investigate the connection between these two problems in more detail.

Filip Mazowiecki, Joanna Ochremiak, Adam Witkowski
Computability on the Countable Ordinals and the Hausdorff-Kuratowski Theorem (Extended Abstract)

While there is a well-established notion of what a computable ordinal is, the question which functions on the countable ordinals ought to be computable has received less attention so far. In order to remedy this, we explore various potential representations of the set of countable ordinals. An equivalence class of representations is then suggested as a standard, as it offers the desired closure properties. With a decent notion of computability on the space of countable ordinals in place, we can then state and prove a computable uniform version of the Hausdorff-Kuratowski theorem.

Arno Pauly
Emergence on Decreasing Sandpile Models

Sand is a proper instance for the study of natural algorithmic phenomena. Idealized square/cubic sand grains moving according to “simple” local toppling rules may exhibit surprisingly “complex” global behaviors. In this paper we explore the language made by words corresponding to fixed points reached by iterating a toppling rule starting from a finite stack of sand grains in one dimension. Using arguments from linear algebra, we give a constructive proof that for all decreasing sandpile rules the language of fixed points is accepted by a finite (Muller) automaton. The analysis is completed with a combinatorial study of cases where the

emergence

of precise regular patterns is formally proven. It extends earlier works presented in [

15

17

], and asks how far can we understand and explain emergence following this track?

Kévin Perrot, Éric Rémila
Lost in Self-Stabilization

Let

$$t_a$$

t

a

and

$$t_b$$

t

b

a pair of relatively prime positive integers. We work on chains of

$$n(t_a + t_b)$$

n

(

t

a

+

t

b

)

agents, each of them forming an upper and rightward directed path of the grid

$$\mathbb {Z}^2$$

Z

2

, from

$$ O = (0, 0)$$

O

=

(

0

,

0

)

to

$$ M = (n t_a, n t_b)$$

M

=

(

n

t

a

,

n

t

b

)

. We are interested on evolution rules such that, at each time step, an agent is randomly chosen on the chain and is allowed to jump to another site of the grid, with preservation of the connectivity of the chain, and the endpoints. The rules must be local, i.e. the decision of jumping or not only depends on the neighborhood of fixed size

$$s$$

s

of the randomly chosen agent, and not on the parameters

$$t_a, t_b, n$$

t

a

,

t

b

,

n

.

In the paper, we design such a rule which, starting from any chain which does not crosses the continuous line segment [

O

,

M

], reorganizes the chain by iterate applications of the rule, in such a way such that it stabilizes into one of the best possible approximations of [

O

,

M

]. The stabilization is reached after

$$O(n(t_a + t_b))^4)$$

O

(

n

(

t

a

+

t

b

)

)

4

)

iterations.

Damien Regnault, Éric Rémila
Equations and Coequations for Weighted Automata

We study weighted automata from both an algebraic and a coalgebraic perspective. In particular, we consider equations and coequations for weighted automata. We prove a duality result that relates sets of equations (congruences) with (certain) subsets of coequations. As a consequence, we obtain two equivalent but complementary ways to define classes of weighted automata. We show that this duality cannot be generalized to linear congruences in general but we obtain partial results when weights are from a field.

Julian Salamanca, Marcello Bonsangue, Jan Rutten
Backmatter
Metadata
Title
Mathematical Foundations of Computer Science 2015
Editors
Giuseppe F Italiano
Giovanni Pighizzini
Donald T. Sannella
Copyright Year
2015
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-662-48057-1
Print ISBN
978-3-662-48056-4
DOI
https://doi.org/10.1007/978-3-662-48057-1

Premium Partner