FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

The Genome Halving Problem is motivated by the whole genome duplication events in molecular evolution that double the gene content of a genome and result in a perfect duplicated genome thatcontains two identical copies of each chromosome. The genome then becomes a subject to rearrangements resulting in some rearranged duplicated genome. The Genome Halving Problem (first introduced and solved by Nadia El-Mabrouk and David Sankoff) is to reconstruct the ancestral pre-duplicated genome from the rearranged duplicated genome. The El-Mabrouk–Sankoff algorithm is rather complex and in this paper we present a simpler algorithm that is based on a generalization of the notion of the breakpoint graph to the case of duplicated genomes. This generalization makes the El-Mabrouk–Sankoff result more transparent and promises to be useful in future studies of genome duplications.

Monolithic finite-state probabilistic programs have been abstractly modeled by finite Markov chains, and the algorithmic verification problems for them have been investigated very extensively. In this paper we survey recent work conducted by the authors together with colleagues on he algorithmic verification of probabilistic procedural programs ([BKS,EKM04,EY04]). Probabilistic procedural programs can more naturally be modeled by

recursive Markov chains

([EY04)], or equivalently,

probabilistic pushdown automata

([EKM04)]. A very rich theory emerges for these models. While our recent work solves a number of verification problems for these models, many intriguing questions remain open.

Computing over data streams is a recent phenomenon that is of growing interest in many areas of computer science, including databases, computer networks and theory of algorithms. In this scenario, it is assumed that the algorithm sees the elements of the input one-by-one in arbitrary order, and needs to compute a certain function of the input. However, it does not have enough memory to store the whole input. Therefore, it must maintain a “sketch” of the data. Designing a sketching method for a given problem is a novel and exciting challenge for algorithm design.

Conventional semantics for shared-variable concurrency suffers from the “grain of time” problem, i.e., the necessity of specifying a default level of atomicity. We propose a semantics that avoids any such choice by regarding all interference that is not controlled by explicit critical regions as catastrophic. It is based on three principles:

Operations have duration and can overlap one another during execution.

If two overlapping operations touch the same location, the meaning of the program execution is “wrong”.

If, from a given starting state, execution of a program can give “wrong”, then no other possibilities need be considered.

Regular languages are central objects of study in computer science. Although they are quite “easy” in the traditional space-time framework of sequential computations, the situation is different when other models are considered.In this paper we consider the subclass of regular languages that can be defined via unambiguous concatenation. We show remarkable algorithmic properties of this class in the context of boolean circuits and in that of computational learning.

We consider

Timed Petri Nets (TPNs)

: extensions of Petri nets in which each token is equipped with a real-valued clock. We consider the following three verification problems for TPNs.

(i)

Zenoness:

whether there is an infinite computation from a given marking which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from [dFERA00].

(ii)

Token Liveness:

whether a token is

alive

in a marking, i.e., whether there is a computation from the marking which eventually consumes the token.We show decidability of the problem by reducing it to the

coverability problem

,which is decidable for TPNs.

(iii)

Boundedness:

whether the size of the reachable markings is bounded. We consider two versions of the problem; namely

semantic boundedness

where only live tokens are taken into consideration in the markings,and

syntactic boundedness

where also dead tokens are considered. We show undecidability of semantic boundedness, while we prove that syntactic boundedness is decidable through an extension of the Karp-Miller algorithm.

We present an algorithm for finding the minimal number of clocks of a given timed automaton recognizing the language described by a so-called

bounded timed regular expressionw

. This algorithm is based on the partition of the timed projection of

w

into so-called

delay cells

. Using this decomposition, we give a method to compute practically this number for

w

. We then apply this technique to prove that for some

n

-clock timed automation we need an additional clock to encode

urgency

.

We characterize aperiodic distributed behaviours, modelled as Mazurkiewicz traces in terms of a very natural cascade product of the

gossip

automaton with a counter-free asynchronous automaton. The characterization strengthens the fundamental results of Schutzenberger and, McNaughton and Papert and implies that star-free, equivalently, first-order-definable trace languages admit counter-free asynchronous acceptors modulo the gossip automaton.

We present a fragment of separation logic oriented to linked lists, and study decision procedures for validity of entailments. The restrictions in the fragment are motivated by the stylized form of reasoning done in example program proofs. The fragment includes a predicate for describing linked list segments (a kind of reachability or transitive closure). Decidability is first proved by semantic means: by showing a small model property that bounds the size of potential countermodels that must be checked. We then provide a complete proof system for the fragment, the termination of which furnishes a second decision procedure.

We show how any BSP tree

${\mathcal T}_P$

for the endpoints of a set of

n

disjoint segments in the plane can be used to obtain a BSP tree of size

$O(n.depth({\mathcal T}_P))$

for the segments themselves, such that the range-searching efficiency remains almost the same. We apply this technique to obtain a BSP tree of size

O

(

n

log

n

) such that

ε

-approximate range searching queries with any constant-complexity convex query range can be answered in

O

(min

ε

> 0

{1/

ε

 + 

k

ε

}log

n

) time, where

k

ε

is the number of segments intersecting the

ε

-extended range. The same result can be obtained for disjoint constant-complexity curves, if we allow the BSP to use splitting curves along the given curves.

We also describe how to construct a linear-size BSP tree for low-density scenes consisting of

n

objects in

${\mathbb R}^{d}$

such that

ε

-approximate range searching with any constant-complexity convex query range can be done in

$O(log n + {\rm min}_{\epsilon > 0}{\{1/\epsilon^{(d-1)}+k_{\epsilon}\}})$

time.

We investigate the class of disjoint NP-pairs under different reductions. The structure of this class is intimately linked to the simulation order of propositional proof systems, and we make use of the relationship between propositional proof systems and theories of bounded arithmetic as the main tool of our analysis. Specifically we exhibit a pair which is complete under strong reductions for all disjoint NP-pairs representable in a theory. We use these pairs to explain the simulation order of NP-pairs under these reductions. As corollaries we also get simplified proofs of results obtained earlier in [3] and [5].

We consider the problem of symbolic reachability analysis of higher-order context-free processes. These models are generalizations of the context-free processes (also called BPA processes) where each process manipulates a data structure which can be seen as a nested stack of stacks. Our main result is that, for any higher-order context-free process, the set of all predecessors of a given regular set of configurations is regular and effectively constructible. This result generalizes the analogous result which is known for level 1 context-free processes. We show that this result holds also in the case of backward reachability analysis under a regular constraint on configurations. As a corollary, we obtain a symbolic model checking algorithm for the temporal logic

E(

U,

X)

with regular atomic predicates, i.e., the fragment of CTL restricted to the

EU

and

EX

modalities.

Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove that in case an optimal strategy exists, we can compute a state-based winning optimal strategy.

We introduce ctm, a process calculus which embodies a notion of trust for global computing systems. In ctm each principal (location) is equipped with a policy, which determines its legal behaviour, and with a protocol, which allows interactions between principals and the flow of information from principals to policies. We elect to formalise policies using a Datalog-like logic, and to express protocols in the process algebra style. This yields an expressive calculus very suitable for the global computing scenarios, and provides a formalisation of notions such as trust evolution. For ctm we define barbed equivalences and study their possible applications.

When studying a 3D convex polyhedron, it is often easier to cut it open and flatten in on the plane. There are several ways to perform this unfolding. Standard unfoldings which have been used in literature include

Star

Unfoldings,

Source

Unfoldings, and

Planar

Unfoldings, each differing only in the cuts that are made. Note that every unfolding has the property that a straight line between two points on this unfolding need not be contained completely within the body of this unfolding. This could potentially lead to situations where the above straight line is shorter than the shortest path between the corresponding end points on the convex polyhedron. We call such straight lines

short-cuts

. The presence of short-cuts is an obstacle to the use of unfoldings for designing algorithms which compute shortest paths on polyhedra. We study various properties of Star, Source and Planar Unfoldings which could play a role in circumventing this obstacle and facilitating the use of these unfoldings for shortest path algorithms.

We begin by showing that Star and Source Unfoldings do not have short-cuts. We also describe a new structure called the

Extended Source

Unfolding which exhibits a similar property. In contrast, it is known that Planar unfoldings can indeed have short-cuts. Using our results on Star, Source and Extended Source Unfoldings above and using an additional structure called the

Compacted Source

Unfolding, we provide a necessary condition for a pair of points on a Planar Unfolding to form a short-cut. We believe that this condition could be useful in enumerating all Shortest Path Edge Sequences on a convex polyhedron in an output-sensitive way, using the Planar Unfolding.

Given two simplicial complexes

${\mathcal C}_{\rm 1}$

and

${\mathcal C}_{\rm 2}$

embedded in Euclidean space

${\mathbb R}^{d}$

,

${\mathcal C}_{\rm 1}$

subdivides

${\mathcal C}_{\rm 2}$

if (

i

)

${\mathcal C}_{\rm 1}$

and

${\mathcal C}_{\rm 2}$

have the same underlying space, and (

ii

) every simplex in

${\mathcal C}_{\rm 1}$

is contained in a simplex in

${\mathcal C}_{\rm 2}$

. In this paper we present a method to compute a set of weighted points whose alpha complex subdivides a given simplicial complex.

Following this, we also show a simple method to approximate a given polygonal object with a set of balls via computing the subdividing alpha complex of the boundary of the object. The approximation is robust and is able to achieve a union of balls whose Hausdorff distance to the object is less than a given positive real number

ε

.

We introduce real-counter automata, which are two-way finite automata augmented with counters that take real values. In contrast to traditional word automata that accept sequences of symbols, real-counter automata accept real words that are bounded and closed real intervals delimited by a finite number of markers. We study the membership and emptiness problems for one-way/two-way real-counter automata as well as those automata further augmented with other unbounded storage devices such as integer-counters and pushdown stacks.

Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes’ results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination.

We investigate the expressive power of existential monadic second-order logic (monadic Σ

1

) on finite transition systems. In particular, we look at its power to express properties that are invariant under forms of bisimulation and compare these to properties expressible in corresponding fixed-point modal calculi. We show that on finite unary transition systems the bisimulation invariant fragment of monadic Σ

1

is equivalent to bisimulation-invariant monadic second order logic itself or, equivalently, the mu-calculus. These results contrast with the situation on infinite structures. Although we show that these results do not extend directly to the case of arbitrary finite transition systems, we are still able to show that the situation there contrasts sharply with the case of arbitrary structures. In particular, we establish a partial expressiveness result by means of tree-like tiling systems that does not hold on infinite structures.

Hilbert posed the following problem as the 17th in the list of 23 problems in his famous 1900 lecture:

Given a multivariate polynomial that takes only non-negative values over the reals, can it be represented as a sum of squares of rational functions?

In 1927, E. Artin gave an affirmative answer to this question. His result guaranteed the existence of such a finite representation and raised the following important question:

What is the

minimum number

of rational functions needed to represent any non-negative n

-variate, degree d

polynomial?

In 1967, Pfister proved that any

n

-variate non-negative polynomial over the reals can be written as sum of squares of at most 2

n

rational functions. In spite of a considerable effort by mathematicians for over 75 years, it is

not

known whether

n

+2 rational functions are sufficient!

In lieu of the lack of progress towards the resolution of this question, we initiate the study of Hilbert’s 17th problem from the point of view of Computational Complexity. In this setting, the following question is a natural relaxation:

What is the

descriptive complexity

of the sum of squares representation (as rational functions) of a non-negative, n

-variate, degree d

polynomial?

We consider

arithmetic circuits

as a natural representation of rational functions. We are able to show, assuming a standard conjecture in complexity theory, that it is impossible that every non-negative,

n

-variate, degree four polynomial can be represented as a sum of squares of a

small

(polynomial in

n

) number of rational functions, each of which has a

small

size arithmetic circuit (over the rationals) computing it.

This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.

We present a simple randomized algorithm for approximating permanents. The algorithm with inputs

A

,

ε

> 0 produces an output

X

A

with (1 − 

ε

)

per

(

A

) ≤ 

X

A

 ≤ (1 + 

ε

)

per

(

A

) for almost all (0-1) matrices

A

. For any positive constant

ε

> 0 , and almost all (0-1) matrices the algorithm runs in time

O

(

n

2

ω

), i.e., almost linear in the size of the matrix, where

ω

=

ω

(

n

) is any function satisfying

ω

(

n

) → ∞ as

n

→ ∞. This improves the previous bound of

O

(

n

3

ω

) for such matrices. The estimator can also be used to estimate the size of a backtrack tree.

This paper deals with distributed control problems by means of distributed games played on Mazurkiewicz traces. The main difference with other notions of distributed games recently introduced is that, instead of having a

local

view, strategies and controllers are able to use a more accurate memory, based on their

causal

view. Our main result states that using the causal view makes the control synthesis problem decidable for series-parallel systems for

all

recognizable winning conditions on finite behaviors, while this problem with local view was proved undecidable even for reachability conditions.

In this paper, we present a general algorithmic schema called “Expand, Enlarge and Check” from which new efficient algorithms for the coverability problem of

WSTS

can be constructed. We show here that our schema allows us to define forward algorithms that decide the coverability problem for several classes of systems for which the Karp and Miller procedure cannot be generalized, and for which no complete forward algorithms were known. Our results have important applications for the verification of parameterized systems and communication protocols.

We consider the problem of computing a minimum weight pseudo-triangulation of a set

${\mathcal S}$

of

n

points in the plane. We first present an

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

-time algorithm that produces a pseudo-triangulation of weight

$O(wt(\mathcal M(\mathcal S)).{\rm log} n)$

which is shown to be asymptotically worst-case optimal, i.e., there exists a point set

${\mathcal S}$

for which every pseudo-triangulation has weight

$\Omega({\rm log} n.wt(\mathcal M(\mathcal S))$

, where

$wt(\mathcal M(\mathcal S))$

is the weight of a minimum spanning tree of

${\mathcal S}$

. We also present a constant factor approximation algorithm running in cubic time. In the process we give an algorithm that produces a minimum weight pseudo-triangulation of a simple polygon.

The join of two sets of facts,

E

1

and

E

2

, is defined as the set of all facts that are implied independently by both

E

1

and

E

2

. Congruence closure is a widely used representation for sets of equational facts in the theory of uninterpreted function symbols (UFS). We present an optimal join algorithm for special classes of the theory of UFS using the abstract congruence closure framework. Several known join algorithms, which work on a strict subclass, can be cast as specific instantiations of our generic procedure. We demonstrate the limitations of any approach for computing joins that is based on the use of congruence closure. We also mention some interesting open problems in this area.

We show that coresets do not exist for the problem of 2-slabs in

${\mathbb R}^{3}$

, thus demonstrating that the natural approach for solving approximately this problem efficiently is infeasible. On the positive side, for a point set

P

in

${\mathbb R}^{3}$

, we describe a near linear time algorithm for computing a (1+

ε

)-approximation to the minimum width 2-slab cover of

P

. This is a first step in providing an efficient approximation algorithm for the problem of covering a point set with

k

-slabs.

We consider three complexity-theoretic hypotheses that have been studied in different contexts and shown to have many plausible consequences.

–

The Measure Hypothesis:

NP does not have

p

-measure 0.

–

The pseudo-

NP

Hypothesis:

there is an NP Language

L

such that any DTIME

$2^{{n^\epsilon}}$

Language L’ can be distinguished from

L

by an NP refuter.

–

The

NP-

Machine Hypothesis:

there is an NP machine accepting 0

*

for which no

$2^{{n^\epsilon}}$

-time machine can find infinitely many accepting computations.

We show that the NP-machine hypothesis is implied by each of the first two. Previously, no relationships were known among these three hypotheses. Moreover, we unify previous work by showing that several derandomization and circuit-size lower bounds that are known to follow from the first two hypotheses also follow from the NP-machine hypothesis. We also consider UP versions of the above hypotheses as well as related immunity and scaled dimension hypotheses.

In this paper we improve the analysis of approximation algorithms based on semidefinite programming for the maximum graph partitioning problems MAX-

k

-CUT, MAX-

k

-UNCUT, MAX-

k

-DIRECTED-CUT, MAX -

k

-DIRECTED-UNCUT, MAX-

k

-DENSE-SUBGRAPH, and MAX-

k

-VERTEX-COVER.It was observed by Han, Ye, Zhang (2002) and Halperin, Zwick (2002) that a parameter-driven random hyperplane can lead to better approximation factors than obtained by Goemans and Williamson (1994). Halperin and Zwick could describe the approximation factors by a mathematical optimization problem for the above problems for

$k=\frac{n}{2}$

and found a choice of parameters in a heuristic way. The innovation of this paper is twofold. First, we generalize the algorithm of Halperin and Zwick to cover all cases of

k

, adding some algorithmic features. The hard work is to show that this leads to a mathematical optimization problem for an optimal choice of parameters. Secondly, as a key-step of this paper we prove that a sub-optimal set of parameters is determined by a

linear program

. Its optimal solution computed by CPLEX leads to the desired improvements. In this fashion a more systematic analysis of the semidefinite relaxation scheme is obtained which leaves room for further improvements.

A computational model for learning languages in the limit from full positive data and a bounded number of queries to the teacher (oracle) is introduced and explored. Equivalence, superset, and subset queries are considered. If the answer is negative, the teacher may provide a counterexample. We consider several types of counterexamples: arbitrary, least counterexamples, and no counterexamples. A number of hierarchies based on the number of queries (answers) and types of answers/ counterexamples is established. Capabilities of learning with different types of queries are compared. In most cases, one or two queries of one type can sometimes do more than any bounded number of queries of another type. Still, surprisingly, a finite number of subset queries is sufficient to simulate the same number of equivalence queries when

behaviourally correct

learners do not receive counterexamples and may have unbounded number of errors in almost all conjectures.

The

k

-

Local Hamiltonian

problem is a natural complete problem for the complexity class

QMA

, the quantum analog of

NP

. It is similar in spirit to

MAX-

k

-SAT

, which is

NP

-complete for

k

≥ 2. It was known that the problem is

QMA

-complete for any

k

≥ 3. On the other hand 1-

Local Hamiltonian

is in

P

, and hence not believed to be

QMA

-complete. The complexity of the 2-

Local Hamiltonian

problem has long been outstanding. Here we settle the question and show that it is

QMA

-complete. We provide two independent proofs; our first proof uses a powerful technique for analyzing the sum of two Hamiltonians; this technique is based on perturbation theory and we believe that it might prove useful elsewhere. The second proof uses elementary linear algebra only. Using our techniques we also show that adiabatic computation with two-local interactions on qubits is equivalent to standard quantum computation.

We derive lower bounds for tradeoffs between the communication

C

and space

S

for communicating circuits. The first such bound applies to quantum circuits. If for any problem

f

:

X

×

Y

→

Z

the multicolor discrepancy of the communication matrix of

f

is 1/2

d

, then any bounded error quantum protocol with space

S

, in which Alice receives some

l

inputs, Bob

r

inputs, and they compute

f

(

x

i

,

y

j

) for the

l

·

r

pairs of inputs (

x

i

,

y

j

) needs communication

C

=Ω (

lrd

log |

Z

| /

S

). In particular,

n

×

n

-matrix multiplication over a finite field

F

requires

C

= Θ (

n

3

log

2

|

F

|/

S

), matrix-vector multiplication

C

= Θ (

n

2

log

2

|

F

|/

S

). We then turn to randomized bounded error protocols, and, utilizing a new direct product result for the one-sided rectangle lower bound on randomized communication complexity, derive the bounds

C

= Ω (

n

3

/

S

2

) for Boolean matrix multiplication and

C

= Ω (

n

2

/

S

2

) for Boolean matrix-vector multiplication. These results imply a separation between quantum and randomized protocols when compared to quantum bounds in [KSW04] and partially answer a question by Beame et al.[BTY94].

A self-stabilizing distributed protocol can recover from any state-corrupting fault. A self-stabilizing protocol is called

adaptive

if its recovery time is proportional to the number of processors hit by the fault. General adaptive protocols are known for the special case of function computations: these are tasks that map static distributed inputs to static distributed outputs. In

reactive

distributed systems, input values at each node change on-line, and dynamic distributed outputs are to be generated in response in an on-line fashion. To date, only some specific reactive tasks have had an adaptive implementation. In this paper we outline the first proof that

all

reactive tasks admit adaptive protocols. The key ingredient of the proof is an algorithm for distributing input values in an adaptive fashion. Our algorithm is optimal, up to a constant factor, in its fault resilience, response time, and recovery time.

The class of visibly pushdown languages has been recently defined as a subclass of context-free languages with desirable closure properties and tractable decision problems. We study visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We establish that, unlike pushdown games with pushdown winning conditions, visibly pushdown games are decidable and are

2Exptime

-complete. We also show that pushdown games against

Ltl

specifications and

Caret

specifications are

3Exptime

-complete. Finally, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of Boolean combinations of

Σ

3

sets. This leads to an alternative proof that visibly pushdown automata are not determinizable and also shows that visibly pushdown games are determined.

A separation context is a client program which does not dereference internals of a module with which it interacts. We use certain “precise” relations to unambiguously describe the storage of a module and prove that separation contexts preserve such relations. We also show that a

simulation

theorem holds for separation contexts, while this is not the case for arbitrary client programs.

In this paper we provide an automaton-based solution to the decision problem for a large set of monadic second-order theories of deterministic tree structures. We achieve it in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of ) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. We conclude the paper with a short discussion of related work.

We present fast distributed algorithms for coloring and (connected) dominating set construction in wireless ad hoc networks. We present our algorithms in the context of Unit Disk Graphs which are known to realistically model wireless networks. Our distributed algorithms take into account the loss of messages due to contention from simultaneous interfering transmissions in the wireless medium.

We present randomized distributed algorithms for (conflict-free) Distance-2 coloring, dominating set construction, and connected dominating set construction in Unit Disk Graphs. The coloring algorithm has a time complexity of

O

(Δ log

2

n

) and is guaranteed to use at most

O

(1) times the number of colors required by the optimal algorithm. We present two distributed algorithms for constructing the (connected) dominating set; the former runs in time

O

(Δ log

2

n

) and the latter runs in time

O

(log

2

n

). The two algorithms differ in the amount of local topology information available to the network nodes.

Our algorithms are geared at constructing Well Connected Dominating Sets (WCDS) which have certain powerful and useful structural properties such as low size, low stretch and low degree. In this work, we also explore the rich connections between WCDS and routing in ad hoc networks. Specifically, we combine the properties of WCDS with other ideas to obtain the following interesting applications:

An online distributed algorithm for collision-free, low latency, low redundancy and high throughput broadcasting.

Distributed capacity preserving backbones for unicast routing and scheduling.

A monotone boolean circuit is said to be

multilinear

if for any

AND

gate in the circuit, the minimal representation of the two input functions to the gate do not have any variable in common. We show that multilinear boolean circuits for bipartite perfect matching require exponential size. In fact we prove a stronger result by characterizing the structure of the smallest multilinear boolean circuits for the problem. We also show that the upper bound on the minimum depth of monotone circuits for perfect matching in general graphs is

O

(

n

).

We consider the problem of determining whether a given set

S

in

${\mathbb R}^{n}$

is

approximately

convex, i.e., if there is a convex set

$K \in {\mathbb R}^{n}$

such that the volume of their symmetric difference is at most

ε

vol

(S)

for some given

ε

. When the set is presented only by a membership oracle and a random oracle, we show that the problem can be solved with high probability using

poly

(

n

)(

c

/

ε

)

n

oracle calls and computation time. We complement this result with an exponential lower bound for the natural algorithm that tests convexity along “random” lines. We conjecture that a simple 2-dimensional version of this algorithm has polynomial complexity.

We introduce a notion of linear hyperconnection (formally denoted

L-hyperpath

) between nodes in a directed hypergraph and relate this notion to existing notions of hyperpaths in directed hypergraphs. We observe that many interesting questions in problem domains such as secret transfer protocols, routing in packet filtered networks, and propositional satisfiability are basically questions about existence of

L

-hyperpaths or about cyclomatic number of directed hypergraphs w.r.t.

L

-hypercycles (the minimum number of hyperedges that need to be deleted to make a directed hypergraph free of

L

-hypercycles). We prove that the

L

-hyperpath existence problem, the cyclomatic number problem, the minimum cyclomatic set problem, and the minimal cyclomatic set problem are each complete for a different level (respectively, NP,

${\it \Sigma}^{p}_{2}$

,

${\it \Pi}^{p}_{2}$

, and DP) of the polynomial hierarchy.

We apply machine learning techniques to verify

safety

properties of

finite state machines

which communicate over

unbounded FIFO channels

. Instead of attempting to iteratively compute the reachable states, we use

Angluin’s L* algorithm

to learn these states symbolically as a regular language. The learnt set of reachable states is then used either to prove that the system is safe, or to produce a valid execution of the system that leads to an unsafe state (

i.e.

to produce a counterexample). Specifically, we assume that we are given a model of the system and we provide a novel procedure which answers both

membership

and

equivalence

queries for a representation of the reachable states. We define a new

encoding

scheme for representing reachable states and their witness execution; this enables the learning algorithm to analyze a larger class of FIFO systems automatically than a naive encoding would allow. We show the upper bounds on the running time and space for our method. We have implemented our approach in Java, and we demonstrate its application to a few case studies.

We use linear time temporal logic formulas to model strategic and extensive form games. This allows us to use temporal tableau to reason about the game structure. We order the nodes of the tableau according to the players’ preferences. Using this, we can derive a decision procedure for reasoning about the equilibria of these games. The main result developed in this paper is that every finite game can be converted into an equivalent bargaining game on temporal tableau, where the players negotiate the equilbrium outcome. The decision method proposed in this paper has a number of merits compared to others that can be found in the growing literature connecting games to logic – it captures a wide variety of game forms, it is easy to understand and implement, and it can be enhanced to take into account bounded rationality assumptions.

Equational tree automata accept terms modulo equational theories, and have been used to model algebraic properties of cryptographic primitives in security protocols. A serious limitation is posed by the fact that alternation leads to undecidability in case of theories like ACU and that of Abelian groups, whereas for other theories like XOR, the decidability question has remained open. In this paper, we give a positive answer to this open question by giving effective reductions of alternating general two-way XOR automata to equivalent one-way XOR automata in 3EXPTIME, which also means that they are closed under intersection but not under complementation. We also show that emptiness of these automata, which is needed for deciding secrecy, can be decided directly in 2EXPTIME, without translating them to one-way automata. A key technique we use is the study of Branching Vector Plus-Minimum Systems (BVPMS), which are a variant of VASS (Vector Addition Systems with States), and for which we prove a pumping lemma allowing us to compute their coverability set in EXPTIME.