CATS 2009 Discussion Track 
Welcome to the CATS 2009 Discussion Track. This is a discussion forum for (some of) the accepted papers for CATS, which will be presented at the conference in Wellington in January, 2009. This forum will serve as a means of discussing these papers in the few months before the conference. Discussion is invited from anyone who is interested in the papers and is willing to contribute.

Not all papers accepted for CATS will necessarily appear here. Authors of accepted papers were given the choice whether or not to include their paper in this track. At the time of writing, there were 12 papers included in the discussion track.

Each paper appears with its title as one of the sub-categories of the Papers category.

This is a new and experimental development, and so there are many unanswered questions here. it is our intention that this will enhance the interactions possible at the meeting itself, as the papers are not introduced for the first time at the conference itself. Naturally we are most interested to hear feedback, and particularly on ways in which this could be improved.

[ 2 comments ] ( 20 views )   |  permalink  |  related link  |   ( 3 / 798 )
Papers 
The authors of papers accepted for CATS 2009 were asked whether they wanted their paper to appear in the discussion track or not. The authors of 12 papers agreed to do so. All accepted papers, whether appearing in the discussion track or not, will appear in the CATS proceedings and will be allocated the same presentation time at the conference. Hence participation in the discussion track is entirely voluntary.

The list of papers in the discussion track is below. Each paper's title is a sub-topic of the Papers topic, and more details and discussion comments are in the relevant sub-topic.

Distributing Frequency-Dependent Data Stream Computations by Sumit Ganguly
Spreading of messages in random graphs by Ching-Lueh Chang and Yuh-Dauh Lyuu
Minimum Cost Homomorphism to Oriented Cycles with Some Loops by Mehdi Karimi and Arvind Gupta
Formal Model of a Protocol Converter by Jing Cao and Albert Nymeyer
Longest Paths in Planar DAGs in Unambiguous Logspace by Nutan Limaye, Meena Mahajan and Prajakta Nimbhorkar
Transformation Rules for Z by Mark Utting, Petra Malik and Ian Toyn
Linear Axis for Planar Straight Line Graphs by Kira Vyatkina
Edge-Selection Heuristics for Computing Tutte Polynomials by David Pearce, Gary Haggard and Gordon Royle
On Process Complexity by Adam Day
Reasoning about a distributed probabilistic system by Ukachukwu Ndukwu and J.W. Sanders
Syntactic Conditions for Invertibility in Sequent Calculi by Peter Chapman
Boolean Affine Approximation with Binary Decision Diagrams by
Kevin Henshall, Peter Schachte, Harald Sondergaard and Leigh Whiting

[ add comment ] ( 10 views )   |  permalink  |   ( 3 / 519 )
Distributing Frequency-Dependent Data Stream Computations 
Title: Distributing Frequency-Dependent Data Stream Computations
Author: Sumit Ganguly
Abstract:
For time-efficiency, data stream computations are often performed in a highly distributed fashion (e.g. internet applications and sensor networks). A distributed computation is modeled as a binary tree, whose leaf nodes contain the input stream fragments \sigma_i, each of which are reduced to a message \phi(\delta_i) that is sent to its parent. Internal nodes compose the messages received from its children using a message composition function and relay the composite message upwards in the tree. Finally, the root node obtains a summary composite message of the input stream fragments and processes it to return an answer. A maximally flexible distributed algorithm is one where all possible computation trees over the same set of leaf nodes compute a correct answer, and each tree is identified with a distinct distributed computation. A basic question here is: what kind of data stream computations can be distributed in a flexible manner? (Feldman et al. 2008) show that any s(m)-space, c(m)-communication complexity data stream algorithm that computes a total and symmetric function of its input stream can be used to simulate a maximally flexible distributed algorithm for computing the same function that uses c(m)-communication, O((s(m))^2)-space and 2^O(s(m))-time for the message composition function. We consider distributed computations for approximating total functions over the frequency vector of a data stream (e.g., estimating frequencies, frequent items, quantiles, etc.). We show that if there is a c(m)-communication data streaming algorithm for computing such a function, then there is a maximally flexible algorithm for computing the same approximation function over the sum of distributed n-dimensional vectors requiring at most c(m)-communication and O(c(m))-space and time for the message composition function. We also show the somewhat surprising result that given an apparently inflexible distributed algorithm (i.e., only one tree is known) for computing an arbitrary approximation to a function of the sum of distributed vectors, there exists a maximally flexible distributed algorithms for the same computation with the above mentioned relation between resource consumed between the two algorithms. This improves previous work in terms of the efficiency and generalization of simulation parameters.

[ add comment ] ( 26 views )   |  permalink  |   ( 2.9 / 549 )
Spreading of messages in random graphs 
Title: Spreading of messages in random graphs
Authors: Ching-Lueh Chang, Yuh-Dauh Lyuu
Abstract:
Chang and Lyuu [Chang and Lyuu, 2008] study the spreading of a message in an Erdos-Renyi random graph G(n, p) starting from a set of vertices that are convinced of the message initially. In their strict-majority scenario, whenever more than half of the neighbors of a vertex v are convinced of a message, v itself also becomes convinced. The spreading proceeds asynchronously until no more vertices can be convinced. Following Chang and Lyuu [Chang and Lyuu, 2008], we derive lower bounds on the minimum number min-seed(n, p) of vertices that need to be convinced initially so that all vertices will be convinced at the end. Our main results are that min-seed(n,p) = \Omega(min{n,n^2 p^2}) and min-seed(n,p) = \Omega(n^{2/3}) hold with high probability. We also consider the case of random seeds. For any sufficiently large constant d > 0 and any s <= n/(d \ln n), we show that if one picks the set of seeds uniformly at random from the family of all s-sized sets, then with high probability, not all vertices will be convinced at the end.

[ 1 comment ] ( 50 views )   |  permalink  |   ( 3 / 463 )
Minimum Cost Homomorphism to Oriented Cycles with Some Loops 
Title: Minimum Cost Homomorphism to Oriented Cycles with Some Loops
Authors: Mehdi Karimi, Arvind Gupta
Abstract:
For digraphs D and H, a homomorphism of D to H is a mapping f : V (D) -> V(H) such that uv \in A(D) implies f(u)f(v) \in A(H). Suppose D and H are two digraphs, and c_i(u), u \in V(D), i \in V(H), are nonnegative real costs. The cost of the homomorphism f of D to H is \Sigma_{u \in V(D)} c_{f(u)}(u). The minimum cost homomorphism for a fixed digraph H, denoted by MinHOM(H), asks whether or not an input digraph D, with nonnegative real costs c_i(u), u \in V(D), i \in V(H), admits a homomorphism f to H and if it admits one, find a homomorphism of minimum cost.

The minimum cost homomorphism problem seems to offer a natural and practical way to model many optimization problems such as list homomorphism problems, retraction and precolouring extension problems, chromatic partition optimization, and applied problems in repair analysis.

Our interest is in proving a dichotomy for minimum cost homomorphism problem: we would like to prove that for each digraph H, MinHOM(H) is polynomial-time solvable, or NP-hard. We say that H is a digraph with some loops, if H has at least one loop. For reflexive digraphs H (every vertex has a loop) the complexity of MinHOM(H) is well understood. In this paper, we obtain a full dichotomy for MinHOM(H) when H is an oriented cycle with some loops. Furthermore, we show that this dichotomy is a remarkable progress toward a dichotomy for oriented graphs with some loops.

[ 1 comment ] ( 51 views )   |  permalink  |   ( 3 / 181 )
Formal Model of a Protocol Converter 
Title: Formal Model of a Protocol Converter
Authors: Jing Cao, Albert Nymeyer
Abstract:
Reuse of components is a burgeoning field in chip design. Shorter time to market and assured quality are just two good reasons to reuse previously engineered components. Problems arise however when chip designers need to interface these components as they typically conform to different standards, or no standards at all. The popular model of interfacing components such as protocols is via a `converter' that translates data between the components. We develop a theoretical model of a converter that will enable two given arbitrary protocols to communicate. This model includes bu®ers. We formally define correctness conditions, and guarantee that the resulting converter satisfies these conditions. We also allow the designer to define his own (CTL) conditions. As well, we allow protocols to be nondeterministic, and we ensure only valid data is sent to the converter. The verification of the conditions is carried out by a model checker (not reported in this work). We have implemented our theoretical model and we present experimental results.

[ add comment ] ( 27 views )   |  permalink  |   ( 3.1 / 492 )
Longest Paths in Planar DAGs in Unambiguous Logspace 
Title: Longest Paths in Planar DAGs in Unambiguous Logspace
Authors: Nutan Limaye, Meena Mahajan, Prajakta Nimbhorkar.
Abstract:
Reachability and distance computation are known to be NL-complete in general graphs, but within UL \cap co-UL if the graphs are planar. However, finding longest paths is known to be NP-complete, even for planar graphs. We show that with the combination of planarity and acyclicity, finding the length of the longest path (and also enumerating one such path) is also in UL \cap co-UL. The result extends to toroidal DAGs as well. We also address the question of when reachability, distance, and longest path are indeed equivalent on DAGs, and give partial bounds. When the number of distinct paths is bounded by a polynomial, counting the number of paths is known to be in NL. We show that for planar DAGs with this promise, counting can be done by a UAuxPDA in polynomial time. The UAuxPDA(poly) bound also holds if we want to compute the number of longest paths, or shortest paths, and this number is bounded by a polynomial (irrespective of the total number of paths). Along the way, we show that counting in general DAGs is possible in LogDCFL provided the number of paths is bounded by a polynomial and the target node is the only sink.

[ add comment ] ( 19 views )   |  permalink  |   ( 2.8 / 620 )
Transformation Rules for Z 
Title: Transformation Rules for Z
Authors: Mark Utting, Petra Malik, Ian Toyn
Abstract:
Z is a formal speci cation language combining typed set theory, predicate calculus, and a schema calculus. This paper describes an extension of Z that allows transformation and reasoning rules to be written in a Z-like notation. This gives a high-level, declarative, way of specifying transformations of Z terms, which makes it easier to build new Z manipulation tools. We describe the syntax and semantics of these rules, plus some example reasoning engines that use sets of rules to manipulate Z terms. The utility of these rules is demonstrated by discussing two sets of rules. One set de nes expansion of Z schema expressions. The other set is used by the ZLive animator to preprocess Z expressions into a form more suitable for animation.

[ add comment ] ( 18 views )   |  permalink  |   ( 2.8 / 600 )
Linear Axis for Planar Straight Line Graphs 
Title: Linear Axis for Planar Straight Line Graphs
Author: Kira Vyatkina
Abstract:
A linear axis is a straight line skeleton for a polygonal shape. The concept of a linear axis \epsilon-equivalent to the medial axis has been introduced and studied for simple polygons and for those with holes. In this paper, we generalize the notions of a linear axis and of \epsilon-equivalence to the case of planar straight line graphs. We show that for some graphs, a linear axis \epsilon-equivalent to the medial axis does not exist, for any \epsilon > 0. However, if the graph vertices are in general position, a sought linear axis does exist for any \epsilon > 0, and can be computed in O(n log n) time in the absence of certain correlations in the graph structure.

[ add comment ] ( 15 views )   |  permalink  |   ( 3 / 630 )
Edge-Selection Heuristics for Computing Tutte Polynomials 
Title: Edge-Selection Heuristics for Computing Tutte Polynomials
Authors: David Pearce, Gary Haggard, Gordon Royle
Abstract:
The Tutte polynomial of a graph, also known as the partition function of the q-state Potts model, is a 2-variable polynomial graph invariant of considerable importance in both combinatorics and statistical physics. It contains several other polynomial invariants, such as the chromatic polynomial and flow polynomial as partial evaluations, and various numerical invariants such as the number of spanning trees as complete evaluations. We have developed the most efficient algorithm to-date for computing the Tutte polynomial of a graph. An important component of the algorithm affecting efficiency is the choice of edge to work on at each stage in the computation. In this paper, we present and discuss two edge-selection heuristics which (respectively) give good performance on sparse and dense graphs. We also present experimental data comparing these heuristics against a range of others to demonstrate their effectiveness.

[ add comment ] ( 17 views )   |  permalink  |   ( 2.9 / 522 )
On Process Complexity 
Title: On Process Complexity
Author: Adam Day
Abstract:
Process complexity is one of the basic variants of Kolmogorov complexity. Unlike plain Kolmogorov complexity, process complexity provides a simple characterization of randomness for real numbers in terms of initial segment complexity. Process complexity was first developed in (Schnorr 1973). Schnorr’s definition of a process, while simple, can be difficult to work with. In many situations, a preferable definition of a process is that given by Levin in (Levin & Zvonkin 1970). In this paper we define a variant of process complexity based on Levin’s definition of a process. We call this variant strict process complexity. Strict process complexity retains the main desirable properties of process complexity. Particularly, it provides simple characterizations of Martin-L¨of random real numbers, and of computable real numbers. However, we will prove that strict process complexity does not agree within an additive constant with Schnorr’s original process complexity. One of the basic properties of prefix-free complexity is that it is subadditive. Subadditive means that there is some constant d such that for all strings \delta, \tau the complexity of \delta\tau (\delta and \tau concatenated) is less than or equal to the sum of the complexities of \delta and \tau plus d. A fundamental question about any complexity measure is whether or not it is subadditive. In this paper we resolve this question for process complexity by proving that neither of these process complexities is subadditive.

[ add comment ] ( 13 views )   |  permalink  |   ( 3 / 553 )
Reasoning about a distributed probabilistic system  
Title: Reasoning about a distributed probabilistic system
Authors: Ukachukwu Ndukwu, J.W. Sanders
Abstract:
Reasoning about a distributed system that exhibits a combination of probabilistic and temporal behaviour does not seem to be easy with current techniques. The reason is the interaction between probability and abstraction (local block), made worse by remote synchronisation. The formalism of process algebra has not so far provided much insight, and so the alternative of shared-variable concurrency has been explored. In this paper the recently proposed language ptsc (for probability, time and shared-variable concurrency) is extended by constructs for interleaving and local block. Both enhance a designer's ability to modularise a design; the latter also permits a design to be compared with its more abstract specification, by concealing appropriately chosen design variables. Laws of the extended language are studied and applied in a case study consisting of a faulty register-transfer-level design.

[ add comment ] ( 19 views )   |  permalink  |   ( 3 / 469 )
Syntactic Conditions for Invertibility in Sequent Calculi  
Title: Syntactic Conditions for Invertibility in Sequent Calculi
Author: Peter Chapman
Abstract:
Formalised proofs of Cut admissibility sometimes rely on the invertibility of the rules of a sequent calculus. We present sufficient conditions for when a rule is invertible with respect to a calculus, which is important for guiding proof search. We illustrate the conditions with examples. It must be noted we give purely syntactic criteria; no guarantees are given as to the suitability of the rules. We also formalise some of the results in the proof assistant Isabelle, as a means to automating Cut admissibility proofs.

[ add comment ] ( 15 views )   |  permalink  |   ( 2.9 / 482 )
Boolean Affine Approximation with Binary Decision Diagrams 
Title: Boolean Affine Approximation with Binary Decision Diagrams
Authors: Kevin Henshall, Peter Schachte, Harald Sondergaard and Leigh Whiting
Abstract:
Selman and Kautz’s work on knowledge compilation has established how approximation (strengthening and/or weakening) of a propositional knowledgebase can be used to speed up query processing, at the expense of completeness. In the classical approach, the knowledge-base is assumed to be presented as a propositional formula in conjunctive normal form (CNF), and Horn functions are used to overand under-approximate it (in the hope that many queries can be answered efficiently using the approximations only). However, other representations are possible, and functions other than Horn can be used for approximations, as long as they have deduction-computational properties similar to those of the Horn functions. Zanuttini has suggested that the class of affine Boolean functions would be especially useful in knowledge compilation and has presented various affine approximation algorithms. Since CNF is awkward for presenting affine functions, Zanuttini considers both a sets-of-models representation and the use of modulo 2 congruence equations. Here we consider the use of reduced ordered binary decision diagrams (ROBDDs), a representation which is more compact than the sets of models and which (unlike modulo 2 congruences) can express any source knowledge-base. We present an ROBDD algorithm to find strongest affine upper-approximations of a Boolean function and we argue its correctness.


[ 2 comments ] ( 27 views )   |  permalink  |   ( 3 / 467 )

| 1 |