@string{brics = "{BRICS}"} @string{daimi = "Department of Computer Science, University of Aarhus"} @string{iesd = "Department of Computer Science, Institute of Electronic Systems, Aalborg University"} @string{rs = "Research Series"} @string{ns = "Notes Series"} @string{ls = "Lecture Series"} @string{ds = "Dissertation Series"} @techreport{BRICS-RS-96-62, author = "Thiagarajan, P. S. and Walukiewicz, Igor", title = "An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces", institution = brics, year = 1996, type = rs, number = "RS-96-62", address = daimi, month = dec, note = "19~pp. Appears in " # lics12 # ", pages 183--194", abstract = "A basic result concerning $LTL$, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences. We present here a smooth extension of this result to the class of partial orders known as Mazurkiewicz traces. These partial orders arise in a variety of contexts in concurrency theory and they provide the conceptual basis for many of the partial order reduction methods that have been developed in connection with $LTL$-specifications.\bibpar We show that $LTrL$, our linear time temporal logic, is equal in expressive power to the first order theory of traces when interpreted over (finite and) {\em infinite} traces. This result fills a prominent gap in the existing logical theory of infinite traces. $LTrL$ also provides a syntactic characterisation of the so called trace consistent (robust) $LTL$-specifications. These are specifications expressed as $LTL$ formulas that do not distiguish between different linearizations of the same trace and hence are amenable to partial order reduction methods", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-61, author = "Soloviev, Sergei", title = "Proof of a Conjecture of {S}. {M}ac {L}ane", institution = brics, year = 1996, type = rs, number = "RS-96-61", address = daimi, month = dec, note = "53~pp. Extended abstract appears in " # lncs953 # ", pages 59--80 Journal version appears in {\em Annals of Pure and Applied Logic}, 90(1--3):101--162, 1997", abstract = "Some sufficient conditions on a Symmetric Monoidal Closed category {\bf K} are obtained such that a diagram in a free SMC category generated by the set ${\bf A}$ of atoms commutes if and only if all its interpretations in {\bf K} are commutative. In particular, the category of vector spaces on any field satisfies these conditions (only this case was considered in the original Mac Lane conjecture). Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent if and only if all their interpretations in {\bf K} are equal. In fact, the assignment of values (objects of {\bf K}) to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R.~Voreadou's proof of the ``abstract coherence theorem'' found by the author, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of S.~Mac Lane conjecture proves also the correctness of the modified description", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-60, author = "Bengtsson, Johan and Larsen, Kim G. and Larsson, Fredrik and Pettersson, Paul and Yi, Wang", title = "{{\sc Uppaal}} in 1995", institution = brics, year = 1996, type = rs, number = "RS-96-60", address = iesd, month = dec, note = "5~pp. Appears in " # lncs1055 # ", pages 431--434", abstract = "{\sc Uppaal} is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata , developed during the past two years. In this paper, we summarize the main features of {\sc Uppaal} in particular its various extensions developed in 1995 as well as applications to various case-studies, review and provide pointers to the theoretical foundation..\bibpar The current version of {\sc Uppaal} is available on the World Wide Web via the {\sc Uppaal} home page \htmladdnormallink{{\tt http://www.docs.uu.se/\-docs/\-rtmv/\-uppaal}} {http://www.docs.uu.se/docs/rtmv/uppaal}", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-59, author = "Larsen, Kim G. and Pettersson, Paul and Yi, Wang", title = "Compositional and Symbolic Model-Checking of Real-Time Systems", institution = brics, year = 1996, type = rs, number = "RS-96-59", address = iesd, month = dec, note = "12~pp. Appears in " # ieeertss95 # ", pages 76--89", abstract = "Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables.\bibpar In this paper we attack these explosion problems by developing and combining {\sl compositional} and {\sl symbolic} model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool {\sc Uppaal}. Experimental results indicate that {\sc Uppaal} performs time- and space-wise favorably compared with other real-time verification tools.", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-58, author = "Bengtsson, Johan and Larsen, Kim G. and Larsson, Fredrik and Pettersson, Paul and Yi, Wang", title = "{{\sc Uppaal}} --- a Tool Suite for Automatic Verification of Real--Time Systems", institution = brics, year = 1996, type = rs, number = "RS-96-58", address = iesd, month = dec, note = "12~pp. Appears in " # lncs1066 # ", pages 232--243", abstract = "{\sc Uppaal} is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a {\sl graphical interface} that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a {\sl compiler} that transforms a certain class of linear hybrid systems to networks of timed automata, and a {\sl model--checker} which is implemented based on constraint--solving techniques. {\sc Uppaal} also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.\bibpar The current version of {\sc Uppaal} is available on the World Wide Web via the {\sc Uppaal} home page \htmladdnormallink{{\tt http://www.docs.uu.se/\-docs/\-rtmv/\-uppaal}} {http://www.docs.uu.se/docs/rtmv/uppaal}", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-57, author = "Larsen, Kim G. and Pettersson, Paul and Yi, Wang", title = "Diagnostic Model-Checking for Real-Time Systems", institution = brics, year = 1996, type = rs, number = "RS-96-57", address = iesd, month = dec, note = "12~pp. Appears in " # lncs1066 # ", pages 575--586", abstract = "{\sc Uppaal} is a new tool suit for automatic verification of networks of timed automata. In this paper we describe the diagnostic model-checking feature of {\sc Uppaal} and illustrates its usefulness through the debugging of (a version of) the Philips Audio-Control Protocol. Together with a graphical interface of {\sc Uppaal} this diagnostic feature allows for a number of errors to be more easily detected and corrected", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-56, author = "Benaissa, Zine-El-Abidine and Lescanne, Pierre and Rose, Kristoffer H.", title = "Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution", institution = brics, year = 1996, type = rs, number = "RS-96-56", address = daimi, month = dec, note = "35~pp. Appears in " # lncs1140 # ", pages 393--407", keywords = "Implementation of functional programming, lambda calculus, weak reduction, explicit substitution, sharing, recursion, space leaks", annote = "Shows how explicit substitution, binding, and addressing, can combine with weak reduction to create a class of low-level computational models for functional programming languages with properties desirable for reasoning about program transformations", abstract = "We {\em present} the $\lambda\sigma_w ^a$-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how $\lambda \sigma_w^a$\ can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely {\em weak reduction strategies}, {\em recursion}, {\em space leaks}, {\em recursive data structures}, and {\em parallel evaluation}, in a uniform way.\bibpar First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing $\lambda$-graph-reduction vs.\ environment-based evaluation. Second, we show how to add {\em constructors and explicit recursion} to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of {\em space leaks} in $\lambda\sigma_w^a$ and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the ``trimming'' performed by the STG machine does not leak space.\bibpar In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-55, author = "Kristoffersen, K{\aa}re J. and Laroussinie, Fran{\c{c}}ois and Larsen, Kim G. and Pettersson, Paul and Yi, Wang", title = "A Compositional Proof of a Real-Time Mutual Exclusion Protocol", institution = brics, year = 1996, type = rs, number = "RS-96-55", address = iesd, month = dec, note = "14~pp. Appears with the title {\em A Compositional Proof of a Mutual Exclusion Protocol} in " # lncs1214 # ", pages 565--579", abstract = "In this paper, we apply a compositional proof technique to an automatic verification of the correctness of Fischer's mutual exclusion protocol. It is demonstrated that the technique may avoid the state--explosion problem. Our compositional technique has recently been implemented in a tool CMC\footnote{CMC: Compositional Model Checking}, which gives experimental evidence that the size of the verification effort required of the technique only grows polynomially in the size of the number of processes in the protocol. In particular, CMC verifies the protocol for 50 processes within 172.3 seconds and using only 32MB main memory. In contrast all existing verification tools for timed systems will suffer from the state--explosion problem, and no tool has to our knowledge succeeded in verifying the protocol for more than $11$ processes", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-54, author = "Walukiewicz, Igor", title = "Pushdown Processes: Games and Model Checking", institution = brics, year = 1996, type = rs, number = "RS-96-54", address = daimi, month = dec, note = "31~pp. Appears in " # lncs1102 # ", pages 62--74. Journal version appears in {\em Information and Computation}, 164:234--263, 2001", abstract = "Games given by transition graphs of pushdown processes are considered. It is shown that if there is a winning strategy in such a game then there is a winning strategy that is realized by a pushdown process. This fact turns out to be connected with the model checking problem for the pushdown automata and the propositional $\mu$-calculus. It is show that this model checking problem is DEXPTIME-complete", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-53, author = "Mosses, Peter D.", title = "Theory and Practice of Action Semantics", institution = brics, year = 1996, type = rs, number = "RS-96-53", address = daimi, month = dec, note = "26~pp. Appears in " # lncs1113 # ", pages 37--61", abstract = "Action Semantics is a framework for the formal description of programming languages. Its main advantage over other frameworks is pragmatic: action-semantic descriptions (ASDs) scale up smoothly to realistic programming languages. This is due to the inherent extensibility and modifiability of ASDs, ensuring that extensions and changes to the described language require only proportionate changes in its description. (In denotational or operational semantics, adding an unforeseen construct to a language may require a reformulation of the entire description.)\bibpar After sketching the background for the development of action semantics, we summarize the main ideas of the framework, and provide a simple illustrative example of an ASD. We identify which features of ASDs are crucial for good pragmatics. Then we explain the foundations of action semantics, and survey recent advances in its theory and practical applications. Finally, we assess the prospects for further development and use of action semantics.\bibpar The action semantics framework was initially developed at the University of Aarhus by the present author, in collaboration with David Watt (University of Glasgow). Groups and individuals scattered around five continents have since contributed to its theory and practice", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-52, author = "Hintermeier, Claus and Kirchner, H{\'e}l{\`e}ne and Mosses, Peter D.", title = "Combining Algebraic and Set-Theoretic Specifications (Extended Version)", institution = brics, year = 1996, type = rs, number = "RS-96-52", address = daimi, month = dec, note = "26~pp. Appears in " # lncs1130 # ", pages 255--274", abstract = "Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we propose an intermediate framework where algebraic specifications are enriched with a set-theoretic type structure, but formulae remain in the logic of equational Horn clauses. This combines an expressive yet modest specification notation with simple semantics and tractable proof theory", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-51, author = "Hintermeier, Claus and Kirchner, H{\'e}l{\`e}ne and Mosses, Peter D.", title = "{$R^n$}- and {$G^n$}-Logics", institution = brics, year = 1996, type = rs, number = "RS-96-51", address = daimi, month = dec, note = "19~pp. Appears in " # lncs1074 # ", pages 90--108", abstract = "Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we propose an intermediate framework where algebraic specifications are enriched with a set-theoretic type structure, but formulae remain in the logic of equational Horn clauses. This combines an expressive yet modest specification notation with simple semantics and tractable proof theory", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-50, author = "Peke{\v c}, Aleksandar", title = "Hypergraph Optimization Problems: Why is the Objective Function Linear?", institution = brics, year = 1996, type = rs, number = "RS-96-50", address = daimi, month = dec, note = "10~pp", abstract = "Choosing an objective function for an optimization problem is a modeling issue and there is no a-priori reason that the objective function must be linear. Still, it seems that linear 0-1 programming formulations are overwhelmingly used as models for optimization problems over discrete structures. We show that this is not an accident. Under some reasonable conditions (from the modeling point of view), the linear objective function is the only possible one", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-49, author = "Andersen, Dan S. and Pedersen, Lars H. and H{\"u}ttel, Hans and Kleist, Josva", title = "Objects, Types and Modal Logics", institution = brics, year = 1996, type = rs, number = "RS-96-49", address = iesd, month = dec, note = "20~pp. Appears in Pierce, editor, {\em 4th International Workshop on the Foundations of Object-Oriented}, FOOL4 Proceedings, 1997", abstract = "In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli. The logic is essentially the modal mu-calculus. The fragment allows us to express the temporal modalities of the logic CTL. We investigate the connection between the type system \mbox{\bf Ob$_{1<:\mu }$} and the mu-calculus, providing a translation of types into modal formulae and an ordering on formulae that is sound w.r.t.\ to the subtype ordering of \mbox{\bf Ob$_{1<:\mu }$}", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-48, author = "Peke{\v c}, Aleksandar", title = "Scalings in Linear Programming: Necessary and Sufficient Conditions for Invariance", institution = brics, year = 1996, type = rs, number = "RS-96-48", address = daimi, month = dec, note = "28~pp", keywords = "Sensitivity Analysis, Scaling, Measurement", abstract = "We analyze invariance of the conclusion of optimality for the linear programming problem under scalings (linear, affine,...) of various problem parameters such as: the coefficients of the objective function, the coefficients of the constraint vector, the coefficients of one or more rows (columns) of the constraint matrix. Measurement theory concepts play a central role in our presentation and we explain why such approach is a natural one", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-47, author = "Peke{\v c}, Aleksandar", title = "Meaningful and Meaningless Solutions for Cooperative $N$-person Games", institution = brics, year = 1996, type = rs, number = "RS-96-47", address = daimi, month = dec, note = "28~pp", keywords = "Cooperative $n$-person Games, Measurement, Sensitivity Analysis", abstract = "Game values often represent data that can be measured in more than one acceptable way (e.g., monetary amounts). We point out that in such cases a statement about cooperative $n$-person game model might be ``meaningless'' in the sense that its truth or falsity depends on the choice of an acceptable way to measure game values. In particular we analyze statements about solution concepts such as the core, stable sets, the nucleolus, the Shapley value (and its generalizations)", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-46, author = "Andreev, Alexander E. and Soloviev, Sergei", title = "A Decision Algorithm for Linear Isomorphism of Types with Complexity {$Cn(log^{2}(n))$}", institution = brics, year = 1996, type = rs, number = "RS-96-46", address = daimi, month = nov, note = "16~pp", abstract = "It is known that ordinary isomorphisms (associativity and commutativity of ``times'', isomorphisms for ``times'' unit and currying) provide a complete axiomatisation for linear isomorphism of types. One of the reasons to consider linear isomorphism of types instead of ordinary isomorphism was that better complexity could be expected. Meanwhile, no upper bounds reasonably close to linear were obtained. We describe an algorithm deciding if two types are linearly isomorphic with complexity $Cn(log^{2}(n))$", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-45, author = "Damg{\aa}rd, Ivan B. and Pedersen, Torben P. and Pfitzmann, Birgit", title = "Statistical Secrecy and Multi-Bit Commitments", institution = brics, year = 1996, type = rs, number = "RS-96-45", address = daimi, month = nov, note = "30~pp. Appears in {\em IEEE Transactions on Information Theory}, 44(3):1143--1151, (1998)", abstract = "We present and compare definitions of the notion of ``statistically hiding'' protocols, and we propose a novel statistically hiding commitment scheme. Informally, a protocol statistically hides a secret if a computationally unlimited adversary who conducts the protocol with the owner of the secret learns almost nothing about it. One definition is based on the $L_1$-norm distance between probability distributions, the other on information theory. We prove that the two definitions are essentially equivalent. For completeness, we also show that statistical counterparts of definitions of computational secrecy are essentially equivalent to our main definitions.\bibpar Commitment schemes are an important cryptologic primitive. Their purpose is to commit one party to a certain value, while hiding this value from the other party until some later time. We present a statistically hiding commitment scheme allowing commitment to many bits. The commitment and reveal protocols of this scheme are constant round, and the size of a commitment is independent of the number of bits committed to. This also holds for the total communication complexity, except of course for the bits needed to send the secret when it is revealed. The proof of the hiding property exploits the equivalence of the two definitions", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-44, author = "Winskel, Glynn", title = "A Presheaf Semantics of Value-Passing Processes", institution = brics, year = 1996, type = rs, number = "RS-96-44", address = daimi, month = nov, note = "23~pp. Extended and revised version of paper appearing in " # lncs1119 # ", pages 98--114", abstract = "This paper investigates presheaf models for process calculi with value passing. Denotational semantics in presheaf models are shown to correspond to operational semantics in that bisimulation obtained from open maps is proved to coincide with bisimulation as defined traditionally from the operational semantics. Both ``early'' and ``late'' semantics are considered, though the more interesting ``late'' semantics is emphasised. A presheaf model and denotational semantics is proposed for a language allowing process passing, though there remains the problem of relating the notion of bisimulation obtained from open maps to a more traditional definition from the operational semantics. A tentative beginning is made of a ``domain theory'' supporting presheaf models.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-43, author = "Ing{\'o}lfsd{\'o}ttir, Anna", title = "Weak Semantics Based on Lighted Button Pressing Experiments: An Alternative Characterization of the Readiness Semantics", institution = brics, year = 1996, type = rs, number = "RS-96-43", address = daimi, month = nov, note = "36~pp. Appears in " # lncs1258 # ", pages 226--243", abstract = "Imposing certain restrictions on the transition system that defines the behaviour of a process allows us to characterize the readiness semantics of Olderog and Hoare by means of black--box testing experiments, or more precisely by the lighted button testing experiments of Bloom and Meyer. As divergence is considered we give the semantics as a preorder, the readiness preorder, which kernel coincides with the readiness equivalence of Olderog and Hoare. This leads to a bisimulation like characterization and a modal characterization of the semantics. A concrete language, recursive free $CCS$ without $\tau$, is introduced, a proof system defined and it is shown to be sound and complete with respect to the readiness preorder. In the completeness proof the modal characterization plays an important role as it allows us to prove algebraicity of the preorder purely operationally", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-42, author = "Brodal, Gerth St{\o}lting and Skyum, Sven", title = "The Complexity of Computing the $k$-ary Composition of a Binary Associative Operator", institution = brics, year = 1996, type = rs, number = "RS-96-42", address = daimi, month = nov, note = "15~pp", abstract = "We show that the problem of computing all contiguous $k$-ary compositions of a sequence of $n$ values under an associative and commutative operator requires $3((k-1)/(k+1))n-$O$(k)$ operations.\bibpar For the operator $\max$ we show in contrast that in the decision tree model the complexity is $\left(1+\Theta(1/\sqrt{k})\right) n-$O$(k)$. Finally we show that the complexity of the corresponding on-line problem for the operator $\max$ is $(2-1/(k-1)) n-$O$(k)$", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-41, author = "Dziembowski, Stefan", title = "The Fixpoint Bounded-Variable Queries are {PSPACE}-Complete", institution = brics, year = 1996, type = rs, number = "RS-96-41", address = daimi, month = nov, note = "16~pp. Appears in " # lncs1258 # ", pages 89--105", abstract = "We study complexity of the evaluation of fixpoint bounded- variable queries in relational databases. We exhibit a finite database such that the problem whether a closed fixpoint formula using only 2 individual variables is satisfied in this database is PSPACE-complete. This clarifies the issues raised by Moshe Vardi ((1995)) {\em Proceedings of the 14th ACM Symposium on Principles of Database Systems}, pages 266--276). We study also the complexity of query evaluation for a number of restrictions of fixpoint logic. In particular we exhibit a sublogic for which the upper bound postulated by Vardi holds", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-40, author = "Brodal, Gerth St{\o}lting and Chaudhuri, Shiva and Radhakrishnan, Jaikumar", title = "The Randomized Complexity of Maintaining the Minimum", institution = brics, year = 1996, type = rs, number = "RS-96-40", address = daimi, month = nov, note = "20~pp. Appears in {\em Nordic Journal of Computing}, 3(4):337--351, 1996 (special issue devoted to Selected Papers of the 5th Scandinavian Workshop on Algorithm Theory (SWAT'96)). Appears in " # lncs1097 # ", pages 4--15", abstract = "The complexity of maintaining a set under the operations {\sf Insert}, {\sf Delete} and {\sf FindMin} is considered. In the comparison model it is shown that any randomized algorithm with expected amortized cost $t$ comparisons per {\sf Insert} and {\sf Delete} has expected cost at least $n/(e2^{2t})-1$ comparisons for {\sf FindMin}. If {\sf FindMin} is replaced by a weaker operation, {\sf FindAny}, then it is shown that a randomized algorithm with constant expected cost per operation exists; in contrast, it is shown that no deterministic algorithm can have constant cost per operation. Finally, a deterministic algorithm with constant amortized cost per operation for an offline version of the problem is given.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-39, author = "H{\"u}ttel, Hans and Shukla, Sandeep", title = "On the Complexity of Deciding Behavioural Equivalences and Preorders -- A Survey", institution = brics, year = 1996, type = rs, number = "RS-96-39", address = iesd, month = oct, note = "36~pp", abstract = "This paper gives an overview of the computational complexity of all the equivalences in the linear/branching time hierarchy and the preorders in the corresponding hierarchy of preorders. We consider {\sf finite state} or {\em regular} processes as well as infinite-state BPA processes.\bibpar A distinction, which turns out to be important in the finite-state processes, is that of {\em simulation-like} equivalences/preorders vs. {\em trace-like} equivalences and preorders. Here we survey various known complexity results for these relations. For regular processes, all simulation-like equivalences and preorders are decidable in polynomial time whereas all trace-like equivalences and preorders are PSPACE-Complete. We also consider interesting special classes of regular processes such as {\em deterministic}, {\em determinate}, {\em unary}, {\em locally unary}, and {\em tree-like} processes and survey the known complexity results in these special cases.\bibpar For infinite-state processes the results are quite different. For the class of {\em context-free processes} or {\em BPA processes} any preorder or equivalence beyond bisimulation is undecidable but bisimulation equivalence is polynomial time decidable for {\em normed} BPA processes and is known to be elementarily decidable in the general case. For the class of {\em BPP} processes, all preorders and equivalences apart from bisimilarity are undecidable. However, bisimilarity is decidable in this case and is known to be decidable in polynomial time for normed BPP processes.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-38, author = "H{\"u}ttel, Hans and Kleist, Josva", title = "Objects as Mobile Processes", institution = brics, year = 1996, type = rs, number = "RS-96-38", address = iesd, month = oct, note = "23~pp. Presented at " # tcsmfps96, abstract = "The object calculus of Abadi and Cardelli is intended as model of central aspects of object-oriented programming languages. In this paper we encode the object calculus in the asynchronous $\pi$-calculus without matching and investigate the properties of our encoding.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-37, author = "Brodal, Gerth St{\o}lting and Okasaki, Chris", title = "Optimal Purely Functional Priority Queues", institution = brics, year = 1996, type = rs, number = "RS-96-37", address = daimi, month = oct, note = "27~pp. Appears in {\em Journal of Functional Programming}, 6(6):839--858, November 1996", abstract = "Brodal recently introduced the first implementation of imperative priority queues to support {\it findMin}, {\it insert}, and {\it meld} in $O(1)$ worst-case time, and {\it deleteMin} in $O(\log n)$ worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues. In this paper, we adapt Brodal's data structure to a purely functional setting. In doing so, we both simplify the data structure and clarify its relationship to the binomial queues of Vuillemin, which support all four operations in $O(\log n)$ time. Specifically, we derive our implementation from binomial queues in three steps: first, we reduce the running time of {\it insert} to $O(1)$ by eliminating the possibility of cascading links; second, we reduce the running time of {\it findMin} to $O(1)$ by adding a global root to hold the minimum element; and finally, we reduce the running time of {\it meld} to $O(1)$ by allowing priority queues to contain other priority queues. Each of these steps is expressed using ML-style functors. The last transformation, known as data-structural bootstrapping, is an interesting application of higher-order functors and recursive structures.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-36, author = "Aceto, Luca and Fokkink, Willem Jan and Ing{\'o}lfsd{\'o}ttir, Anna", title = "On a Question of {A}.~{S}alomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based", institution = brics, year = 1996, type = rs, number = "RS-96-36", address = iesd, month = oct, note = "16~pp. Appears in {\em Theoretical Computer Science}, 209(1--2):141--162, December 1998", abstract = "Salomaa ((1969) {\em Theory of Automata}, page 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway ((1971) {\em Regular Algebra and Finite Machines}, page 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway {\sl ibidem}.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-35, author = "Cattani, Gian Luca and Winskel, Glynn", title = "Presheaf Models for Concurrency", institution = brics, year = 1996, type = rs, number = "RS-96-35", address = daimi, month = oct, note = "16~pp. Appears in " # lncs1258 # ", pages 58--75", abstract = "This paper studies presheaf models for concurrent computation. An aim is to harness the general machinery around presheaves for the purposes of process calculi. Traditional models like synchronisation trees and event structures have been shown to embed fully and faithfully in particular presheaf models in such a way that bisimulation, expressed through the presence of a span of open maps, is conserved. As is shown in the work of Joyal and Moerdijk, presheaves are rich in constructions which preserve open maps, and so bisimulation, by arguments of a very general nature. This paper contributes similar results but biased towards questions of bisimulation in process calculi. It is concerned with modelling process constructions on presheaves, showing these preserve open maps, and with transferring such results to traditional models for processes. One new result here is that a wide range of left Kan extensions, between categories of presheaves, preserve open maps. As a corollary, this also implies that any colimit-preserving functor between presheaf categories preserves open maps. A particular left Kan extension is shown to coincide with a refinement operation on event structures. A broad class of presheaf models is proposed for a general process calculus. General arguments are given for why the operations of a presheaf model preserve open maps and why for specific presheaf models the operations coincide with those of traditional models.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-34, author = "Hatcliff, John and Danvy, Olivier", title = "A Computational Formalization for Partial Evaluation (Extended Version)", institution = brics, year = 1996, type = rs, number = "RS-96-34", address = daimi, month = oct, note = "67~pp. Appears in {\em Mathematical Structures in Computer Science}, 7(5):507--541, " # oct # " 1997", abstract = "We formalize a partial evaluator for Eugenio Moggi's computational metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding, and enables us to express the essence of ``control-based binding-time improvements'' for let expressions. Specifically, we prove that the binding-time improvements given by ``continuation-based specialization'' can be expressed in the metalanguage via monadic laws.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-96-33, author = "Buss, Jonathan F. and Frandsen, Gudmund Skovbjerg and Shallit, Jeffrey Outlaw", title = "The Computational Complexity of Some Problems of Linear Algebra", institution = brics, year = 1996, type = rs, number = "RS-96-33", address = daimi, month = sep, note = "39~pp. Revised version appears in " # lncs1200 # ", pages 451--462 and later in {\em Journal of Computer and System Sciences}, 58(3):572--596, 1998", abstract = "We consider the computational complexity of some problems dealing with matrix rank. Let $E, S$ be subsets of a commutative ring $R$. Let $x_1, x_2, \ldots, x_t$ be variables. Given a matrix $M = M(x_1, x_2, \ldots, x_t)$ with entries chosen from $E \cup\lbrace x_1, x_2, \ldots, x_t \rbrace$, we want to determine $${\rm maxrank}_S (M) = \max_{(a_1, a_2, \ldots , a_t) \in S^t} {\rm rank\ }M(a_1, a_2, \ldots a_t)$$ and $${\rm minrank}_S (M) = \min_{(a_1, a_2, \ldots, a_t) \in S^t} {\rm rank\ }M(a_1, a_2, \ldots a_t).$$ There are also variants of these problems that specify more about the structure of $M$, or instead of asking for the minimum or maximum rank, ask if there is some substitution of the variables that makes the matrix invertible or non invertible.\bibpar Depending on $E, S$, and on which variant is studied, the complexity of these problems can range from polynomial-time solvable to random polynomial-time solvable to {\it NP}-complete to {\it PSPACE}-solvable to unsolvable.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-32, author = "Thiagarajan, P. S.", title = "Regular Trace Event Structures", institution = brics, year = 1996, type = rs, number = "RS-96-32", address = daimi, month = sep, note = "34~pp", abstract = "We propose trace event structures as a starting point for constructing {\em effective} branching time temporal logics in a non-interleaved setting. As a first step towards achieving this goal, we define the notion of a regular trace event structure. We then provide some simple characterizations of this notion of regularity both in terms of recognizable trace languages and in terms of finite 1-safe Petri nets.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-31, author = "Stark, Ian", title = "Names, Equations, Relations: Practical Ways to Reason about `new'", institution = brics, year = 1996, type = rs, number = "RS-96-31", address = daimi, month = sep, note = "ii+22~pp. Please refer to the revised version \htmladdnormallink {BRICS-RS-97-39}{http://www.brics.dk/RS/97/39/}", abstract = "The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to other kinds of local declaration, and to the mobile processes of the pi-calculus.\bibpar This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-30, author = "Andersson, Arne and Miltersen, Peter Bro and Thorup, Mikkel", title = "Fusion Trees can be Implemented with {$AC^0$} Instructions only", institution = brics, year = 1996, type = rs, number = "RS-96-30", address = daimi, month = sep, note = "8~pp. Appears in {\em Theoretical Computer Science}, 215(1--2):337--344, 1999", abstract = "Addressing a problem of Fredman and Willard, we implement fusion trees in deterministic linear space using $AC^0$ instructions only.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-29, author = "Arge, Lars", title = "The {I/O}-Complexity of Ordered Binary-Decision Diagram Manipulation", institution = brics, year = 1996, type = rs, number = "RS-96-29", address = daimi, month = aug, note = "35 pp. An extended abstract version appears in " # lncs1004 # ", pages 82--91", abstract = "Ordered Binary-Decision Diagrams (OBDD) are the state-of-the-art data structure for boolean function manipulation and there exist several software packages for OBDD manipulation. OBDDs have been successfully used to solve problems in e.g. digital-systems design, verification and testing, in mathematical logic, concurrent system design and in artificial intelligence. The OBDDs used in many of these applications quickly get larger than the avaliable main memory and it becomes essential to consider the problem of minimizing the Input/Output (I/O) communication. In this paper we analyze why existing OBDD manipulation algorithms perform poorly in an I/O environment and develop new I/O-efficient algorithms.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-28, author = "Arge, Lars", title = "The Buffer Tree: A New Technique for Optimal {I/O} Algorithms", institution = brics, year = 1996, type = rs, number = "RS-96-28", address = daimi, month = aug, note = "34~pp. This report is a revised and extended version of the BRICS Report~RS-94-16. An extended abstract appears in " # lncs955 # ", pages 334--345", abstract = "In this paper we develop a technique for transforming an internal-memory tree data structure into an external-memory structure. We show how the technique can be used to develop a search tree like structure, a priority queue, a (one-dimensional) range tree and a segment tree, and give examples of how these structures can be used to develop efficient I/O algorithms. All our algorithms are either extremely simple or straightforward generalizations of known internal-memory algorithms---given the developed external data structures. We believe that algorithms relying on the developed structure will be of practical interest due to relatively small constants in the asymptotic bounds.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-27, author = "Dubhashi, Devdatt P. and Priebe, Volker and Ranjan, Desh", title = "Negative Dependence Through the {FKG} Inequality", institution = brics, year = 1996, type = rs, number = "RS-96-27", address = daimi, month = jul, note = "15~pp", abstract = "We investigate random variables arising in occupancy problems, and show the variables to be negatively associated, that is, negatively dependent in a strong sense. Our proofs are based on the FKG correlation inequality, and they suggest a useful, general technique for proving negative dependence among random variables. We also show that in the special case of two binary random variables, the notions of negative correlation and negative association coincide.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-26, author = "Klarlund, Nils and Rauhe, Theis", title = "{BDD} Algorithms and Cache Misses", institution = brics, year = 1996, type = rs, number = "RS-96-26", address = daimi, month = jul, note = "15~pp", abstract = "Within the last few years, CPU speed has greatly overtaken memory speed. For this reason, implementation of symbolic algorithms---with their extensive use of pointers and hashing---must be reexamined.\bibpar In this paper, we introduce the concept of {\em cache miss complexity} as an analytical tool for evaluating algorithms depending on pointer chasing. Such algorithms are typical of symbolic computation found in verification.\bibpar We show how this measure suggests new data structures and algorithms for multi-terminal BDDs. Our ideas have been implemented in a BDD package, which is used in a decision procedure for the Monadic Second-order Logic on strings.\bibpar Experimental results show that on large examples involving e.g\ the verification of concurrent programs, our implementation runs 4 to 5 times faster than a widely used BDD implementation.\bibpar We believe that the method of cache miss complexity is of general interest to any implementor of symbolic algorithms used in verification.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-25, author = "Dubhashi, Devdatt P. and Ranjan, Desh", title = "Balls and Bins: A Study in Negative Dependence", institution = brics, year = 1996, type = rs, number = "RS-96-25", address = daimi, month = jul, note = "27~pp. Appears in {\em Random Structures and Algorithms} 13(2):99--124, 1998", abstract = "This paper investigates the notion of negative dependence amongst random variables and attempts to advocate its use as a simple and unifying paradigm for the analysis of random structures and algorithms.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-24, author = "Jensen, Henrik Ejersbo and Larsen, Kim G. and Skou, Arne", title = "Modelling and Analysis of a Collision Avoidance Protocol using {SPIN} and {UPPAAL}", institution = brics, year = 1996, type = rs, number = "RS-96-24", address = iesd, month = jul, note = "20~pp. Appears in " # amsspin96 # ", pages 33--47", abstract = "This paper compares the tools SPIN and UPPAAL by modelling and verifying a Collision Avoidance Protocol for an Ethernet-like medium. We find that SPIN is well suited for modelling the untimed aspects of the protocol processes and for expressing the relevant (untimed) properties. However, the modelling of the media becomes awkward due to the lack of broadcast communication in the PROMELA language. On the other hand we find it easy to model the timed aspects using the UPPAAL tool. Especially, the notion of {\em committed locations} supports the modelling of broadcast communication. However, the property language of UPPAAL lacks some expessivity for verification of bounded liveness properties, and we indicate how timed testing automata may be constructed for such properties, inspired by the (untimed) checking automata of SPIN", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-23, author = "Aceto, Luca and Fokkink, Willem Jan and Ing{\'o}lfsd{\'o}ttir, Anna", title = "A Menagerie of Non-Finitely Based Process Semantics over {BPA}$^*$: From Ready Simulation Semantics to Completed Tracs", institution = brics, year = 1996, type = rs, number = "RS-96-23", address = iesd, month = jul, note = "38~pp", abstract = "Fokkink and Zantema ((1994) {\em Computer Journal}~{\bf 37}:259--267) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary Kleene star operation (BPA$^*$). In light of this positive result on the mathematical tractability of bisimulation equivalence over BPA$^*$, a natural question to ask is whether any other (pre)congruence relation in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence, none of the preorders and equivalences in van Glabbeek's linear time/branching time spectrum, whose discriminating power lies in between that of ready simulation and that of completed traces, has a finite equational axiomatization. This we achieve by exhibiting a family of (in)equivalences that holds in ready simulation semantics, the finest semantics that we consider, whose instances cannot all be proven by means of any finite set of (in)equations that is sound in completed trace semantics, which is the coarsest semantics that is appropriate for the language BPA$^*$. To this end, for every finite collection of (in)equations that are sound in completed trace semantics, we build a model in which some of the (in)equivalences of the family under consideration fail. The construction of the model mimics the one used by Conway ((1971) {\em Regular Algebra and Finite Machines}, page 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions.\bibpar Our non-finite axiomatizability results apply to the language BPA$^*$ over an arbitrary non-empty set of actions. In particular, % when the set of actions is a singleton, our proof of the fact we show that completed trace equivalence is not finitely based over BPA$^*$ even when the set of actions is a singleton. Our proof of this result may be easily adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa ((1969) {\em Theory of Automata}, page 143).\bibpar Another semantics that is usually considered in process theory is trace semantics. Trace semantics is, in general, not preserved by sequential composition, and is therefore inappropriate for the language BPA$^*$. We show that, if the set of actions is a singleton, trace equivalence and preorder are preserved by all the operators in the signature of BPA$^*$, and coincide with simulation equivalence and preorder, respectively. In that case, unlike all the other semantics considered in this paper, trace semantics have finite, complete equational axiomatizations over closed terms.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-22, author = "Aceto, Luca and Fokkink, Willem Jan", title = "An Equational Axiomatization for Multi-Exit Iteration", institution = brics, year = 1996, type = rs, number = "RS-96-22", address = iesd, month = jun, note = "30~pp. Appears in {\em Information and Computation}, 137(2):121--158, 1997.", abstract = "This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form \begin{eqnarray*} X_1 & = & P_1 X_2 + Q_1 \\ & \vdots& \\ X_n & = & P_n X_1 + Q_n \end{eqnarray*} where $n$ is a positive integer, and the $P_i$ and the $Q_i$ are process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA$^*$). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA$^*$. An expressiveness hierarchy for the family of $k$-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-21, author = "Breslauer, Dany and Jiang, Tao and Jiang, Zhigen", title = "Rotation of Periodic Strings and Short Superstrings", institution = brics, year = 1996, type = rs, number = "RS-96-21", address = daimi, month = jun, note = "14~pp. Appears in {\em Journal of Algorithms}, 24(2):340--353, " # aug # " 1997", abstract = "This paper presents two simple approximation algorithms for the shortest superstring problem, with approximation ratios $2 {2\over 3}$ ($\approx 2.67$) and $2 {25\over 42}$ ($\approx 2.596$), improving the best previously published $2 {3\over 4}$ approximation. The framework of our improved algorithms is similar to that of previous algorithms in the sense that they construct a superstring by computing some optimal cycle covers on the distance graph of the given strings, and then break and merge the cycles to finally obtain a Hamiltonian path, but we make use of new bounds on the overlap between two strings. We prove that for each periodic semi-infinite string $\alpha= a_1 a_2 \cdots$ of period $q$, there exists an integer $k$, such that for {\em any} (finite) string $s$ of period $p$ which is {\em inequivalent} to $\alpha$, the overlap between $s$ and the {\em rotation} $\alpha[k] = a_k a_{k+1} \cdots$ is at most $p+{1\over 2}q$. Moreover, if $p \leq q$, then the overlap between $s$ and $\alpha [k]$ is not larger than ${2\over 3}(p+q)$. In the previous shortest superstring algorithms $p+q$ was used as the standard bound on overlap between two strings with periods $p$ and $q$.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-20, author = "Danvy, Olivier and Lawall, Julia L.", title = "Back to Direct Style {II}: First-Class Continuations", institution = brics, year = 1996, type = rs, number = "RS-96-20", address = daimi, month = jun, note = "36~pp. A preliminary version of this paper appeared in the proceedings of the 1992 ACM Conference on {\em Lisp and Functional Programming}, William Clinger, editor, LISP Pointers, Vol.~V, No.~1, pages 299--310, San Francisco, California, June 1992. ACM Press.", abstract = "The direct-style transformation aims at mapping continuation-passing programs back to direct style, be they originally written in continuation-passing style or the result of the continuation-passing-style transformation. In this paper, we continue to investigate the direct-style transformation by extending it to programs with first-class continuations.\bibpar First-class continuations break the stack-like discipline of continuations in that they are sent results out of turn. We detect them syntactically through an analysis of continuation-passing terms. We conservatively extend the direct-style transformation towards call-by-value functional terms (the pure $\lambda$-calculus) by translating the declaration of a first-class continuation using the control operator call/cc, and by translating an occurrence of a first-class continuation using the control operator throw. We prove that our extension and the corresponding extended continuation-passing-style transformation are inverses.\bibpar Both the direct-style (DS) and continuation-passing-style (CPS) transformations can be generalized to a richer language. These transformations have a place in the programmer's toolbox, and enlarge the class of programs that can be manipulated on a semantic basis. We illustrate both with two applications: the conversion between CPS and DS of an interpreter hand-written in CPS, and the specialization of a coroutine program, where coroutines are implemented using call/cc. The latter example achieves a first: a static coroutine is executed statically and its computational content is inlined in the residual program.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-19, author = "Hatcliff, John and Danvy, Olivier", title = "Thunks and the $\lambda$-Calculus", institution = brics, year = 1996, type = rs, number = "RS-96-19", address = daimi, month = jun, note = "22~pp. Appears in {\em Journal of Functional Programming} 7(3):303--319 (1997)", abstract = "Thirty-five years ago, thunks were used to simulate call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the $\lambda$-calculus. We connect all three of these classical simulations by factorizing the continuation-based call-by-name simulation ${\cal C}_n$ with a thunk-based call-by-name simulation ${\cal T}$ followed by the continuation-based call-by-value simulation ${\cal C}_v$ extended to thunks.\bibpar We show that ${\cal T}$ actually satisfies all of Plotkin's correctness criteria for ${\cal C}_n$ (i.e., his Indifference, Simulation, and Translation theorems). Furthermore, most of the correctness theorems for ${\cal C}_n$ can now be seen as simple corollaries of the corresponding theorems for ${\cal C}_v$ and ${\cal T}$.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-18, author = "Hildebrandt, Thomas Troels and Sassone, Vladimiro", title = "Comparing Transition Systems with Independence and Asynchronous Transition Systems", institution = brics, year = 1996, type = rs, number = "RS-96-18", address = daimi, month = jun, note = "14~pp. Appears in " # lncs1119 # ", pages 84--97", abstract = "Transition systems with independence and asynchronous transition systems are {\it noninterleaving} models for concurrency arising from the same simple idea of decorating transitions with events. They differ for the choice of a {\it derived} versus a {\it primitive} notion of event which induces considerable differences and makes the two models suitable for different purposes. This opens the problem of investigating their mutual relationships, to which this paper gives a fully comprehensive answer.\bibpar In details, we characterise the category of {\it extensional} asynchronous transitions systems as the largest full subcategory of the category of (labelled) asynchronous transition systems which admits ${\sf TSI}$, the category of transition systems with independence, as a {\it coreflective} subcategory. In addition, we introduce {\it event-maximal} asynchronous transitions systems and we show that their category is {\it equivalent} to ${\sf TSI}$, so providing an exhaustive characterisation of transition systems with independence in terms of asynchronous transition systems.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-17, author = "Danvy, Olivier and Malmkj{\ae}r, Karoline and Palsberg, Jens", title = "Eta-Expansion Does {T}he {T}rick (Revised Version)", institution = brics, year = 1996, type = rs, number = "RS-96-17", address = daimi, month = may, note = "29~pp. Appears in {\em ACM Transactions on Programming Languages and Systems}, 8(6):730--751, 1996", abstract = "Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such ``binding-time improvements'': non-standard use of continuation-passing style, eta-expansion, and a popular transformation called ``The Trick''. We provide a unified view of these binding-time improvements, from a typing perspective.\bibpar Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the non-standard use of continuation-passing style encountered in partial evaluation. Eta-expansion thus acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it enables ``The Trick''.\bibpar In this paper, we extend Gomard and Jones's partial evaluator for the $\lambda$-calculus, $\lambda$-Mix, with products and disjoint sums; we point out how eta-expansion for (finite) disjoint sums enables The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to $\lambda $-Mix.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-16, author = "Fajstrup, Lisbeth and Rau{\ss}en, Martin", title = "Detecting Deadlocks in Concurrent Systems", institution = brics, year = 1996, type = rs, number = "RS-96-16", address = iesd, month = may, note = "10~pp. Appears in " # lncs1466 # ", pages 332--347", abstract = "We use a geometric description for deadlocks occurring in scheduling problems for concurrent systems to construct a partial order and hence a directed graph, in which the local maxima correspond to deadlocks. Algorithms finding deadlocks are described and assessed", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-15, author = "Danvy, Olivier", title = "Pragmatic Aspects of Type-Directed Partial Evaluation", institution = brics, year = 1996, type = rs, number = "RS-96-15", address = daimi, month = may, note = "27~pp. Appears in " # lncs1110 # ", pages 73--94", abstract = "Type-directed partial evaluation stems from the residualization of static values in dynamic contexts, given their type and the type of their free variables. Its algorithm coincides with the algorithm for coercing a subtype value into a supertype value, which itself coincides with Berger and Schwichtenberg's normalization algorithm for the simply typed $\lambda $-calculus. Type-directed partial evaluation thus can be used to specialize a compiled, closed program, given its type.\bibpar Since Similix, let-insertion is a cornerstone of partial evaluators for call-by-value procedural languages with computational effects (such as divergence). It prevents the duplication of residual computations, and more generally maintains the order of dynamic side effects in the residual program.\bibpar This article describes the extension of type-directed partial evaluation to insert residual let expressions. This extension requires the user to annotate arrow types with effect information. It is achieved by delimiting and abstracting control, comparably to continuation-based specialization in direct style. It enables type-directed partial evaluation of programs with effects (e.g., a definitional lambda-interpreter for an imperative language) that are in direct style. The residual programs are in A-normal form. A simple corollary yields CPS (continuation-passing style) terms instead. We illustrate both transformations with two interpreters for Paulson's Tiny language, a classical example in partial evaluation.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-14, author = "Danvy, Olivier and Malmkj{\ae}r, Karoline", title = "On the Idempotence of the {CPS} Transformation", institution = brics, year = 1996, type = rs, number = "RS-96-14", address = daimi, month = may, note = "17~pp", abstract = "The CPS (continuation-passing style) transformation on typed $\lambda$-terms has an interpretation in many areas of Computer Science, such as programming languages and type theory. Programming intuition suggests that it in effect, it is idempotent, but this does not directly hold for all existing CPS transformations (Plotkin, Reynolds, Fischer, {\em etc}.).\bibpar We rephrase the call-by-value CPS transformation to make it syntactically idempotent, modulo $\eta$-reduction of the newly introduced continuation. Type-wise, iterating the transformation corresponds to refining the polymorphic domain of answers" } @techreport{BRICS-RS-96-13, author = "Danvy, Olivier and Vestergaard, Ren{\'e}", title = "Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation", institution = brics, year = 1996, type = rs, number = "RS-96-13", address = daimi, month = may, note = "28~pp. Appears in " # lncs1140 # ", pages 182--197", abstract = "We illustrate a simple and effective solution to semantics-based compiling. Our solution is based on type-directed partial evaluation, where \begin{itemize} \item our compiler generator is expressed in a few lines, and is efficient; \item its input is a well-typed, purely functional definitional interpreter in the manner of denotational semantics; \item the output of the generated compiler is three-address code, in the fashion and efficiency of the Dragon Book; \item the generated compiler processes several hundred lines of source code per second. \end{itemize} The source language considered in this case study is imperative, block-structured, higher-order, call-by-value, allows subtyping, and obeys stack discipline. It is bigger than what is usually reported in the literature on semantics-based compiling and partial evaluation.\bibpar Our compiling technique uses the first Futamura projection, i.e., we compile programs by specializing a definitional interpreter with respect to this program.\bibpar Our definitional interpreter is completely straightforward, stack-based, and in direct style. In particular, it requires no clever staging technique (currying, continuations, binding-time improvements, etc.), nor does it rely on any other framework (attribute grammars, annotations, etc.) than the typed lambda-calculus. In particular, it uses no other program analysis than traditional type inference.\bibpar The overall simplicity and effectiveness of the approach has encouraged us to write this paper, to illustrate this genuine solution to denotational semantics-directed compilation, in the spirit of Scott and Strachey.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-12, author = "Arge, Lars and Vengroff, Darren Erik and Vitter, Jeffrey Scott", title = "External-Memory Algorithms for Processing Line Segments in Geographic Information Systems", institution = brics, year = 1996, type = rs, number = "RS-96-12", address = daimi, month = may, note = "34~pp. To appear in {\em Algorithmica}. A shorter version of this paper appears in " # lncs979 # ", pages 295--310", abstract = "In the design of algorithms for large-scale applications it is essential to consider the problem of minimizing I/O communication. Geographical information systems (GIS) are good examples of such large-scale applications as they frequently handle huge amounts of spatial data. In this paper we develop efficient new external-memory algorithms for a number of important problems involving line segments in the plane, including trapezoid decomposition, batched planar point location, triangulation, red-blue line segment intersection reporting, and general line segment intersection reporting. In GIS systems, the first three problems are useful for rendering and modeling, and the latter two are frequently used for overlaying maps and extracting information from them.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-96-11, author = "Dubhashi, Devdatt P. and Grable, David A. and Panconesi, Alessandro", title = "Near-Optimal, Distributed Edge Colouring via the Nibble Method", institution = brics, year = 1996, type = rs, number = "RS-96-11", address = daimi, month = may, note = "17~pp. Appears in " # lncs979 # ", pages 448--459. Appears in the special issue of {\em Theoretical Computer Science\/}, 203(2):225--251, August 1998, devoted to the proceedings of ESA~'95", abstract = "We give a distributed randomized algorithm to edge colour a network. Let $G$ be a graph with $n$ nodes and maximum degree $\Delta$. Here we prove: \begin{itemize} \item If $\Delta= \Omega(\log^{1+\delta} n)$ for some $\delta>0$ and $\lambda> 0$ is fixed, the algorithm almost always colours $G$ with $(1+\lambda)\Delta$ colours in time $O(\log n)$. \item If $s > 0$ is fixed, there exists a positive constant $k$ such that if $\Delta= \Omega(\log^k n)$, the algorithm almost always colours $G$ with $\Delta+ \Delta/\log ^s n = (1+o(1))\Delta$ colours in time $O(\log n + \log^s n \log\log n)$. \end{itemize} By ``almost always'' we mean that the algorithm may fail, but the failure probability can be made arbitrarily close to 0.\bibpar The algorithm is based on the nibble method, a probabilistic strategy introduced by Vojt{\v {e}}ch R{\"o}dl. The analysis makes use of a powerful large deviation inequality for functions of independent random variables.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-10, author = "Bra{\"u}ner, Torben and de Paiva, Valeria", title = "Cut-Elimination for Full Intuitionistic Linear Logic", institution = brics, year = 1996, type = rs, number = "RS-96-10", address = daimi, month = apr, note = "27~pp. Also available as Technical Report 395, Computer Laboratory, University of Cambridge.", abstract = "We describe in full detail a solution to the problem of proving the cut elimination theorem for FILL, a variant of (multiplicative and exponential-free) Linear Logic introduced by Hyland and de Paiva. Hyland and de Paiva's work used a term assignment system to describe FILL and barely sketched the proof of cut elimination. In this paper, as well as correcting a small mistake in their paper and extending the system to deal with exponentials, we introduce a different formal system describing the intuitionistic character of FILL and we provide a full proof of the cut elimination theorem. The formal system is based on a notion of dependency between formulae within a given proof and seems of independent interest. The procedure for cut elimination applies to (classical) multiplicative Linear Logic, and we can (with care) restrict our attention to the subsystem FILL. The proof, as usual with cut elimination proofs, is a little involved and we have not seen it published anywhere.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-9, author = "Husfeldt, Thore and Rauhe, Theis and Skyum, S{\o}ren", title = "Lower Bounds for Dynamic Transitive Closure, Planar Point Location, and Parentheses Matching", institution = brics, year = 1996, type = rs, number = "RS-96-9", address = daimi, month = apr, note = "11~pp. Appears in {\em Nordic Journal of Computing}, 3(4):323--336, " # dec # " 1996. Also in " # lncs1097 # ", pages 198--211", abstract = "We give a number of new lower bounds in the cell probe model with logarithmic cell size, which entails the same bounds on the random access computer with logarithmic word size and unit cost operations.\bibpar We study the signed prefix sum problem: given a string of length $n$ of zeroes and signed ones, compute the sum of its $i$th prefix during updates. We show a lower bound of $\Omega(\log n/\log\log n)$ time per operations, even if the prefix sums are bounded by $\log n/\log\log n$ during all updates. We also show that if the update time is bounded by the product of the worst-case update time and the answer to the query, then the update time must be $\Omega\big (\surd(\log n/\log\log n)\big)$.\bibpar These results allow us to prove lower bounds for a variety of seemingly unrelated dynamic problems. We give a lower bound for the dynamic planar point location in monotone subdivisions of $\Omega(\log n/\log\log n)$ per operation. We give a lower bound for the dynamic transitive closure problem on upward planar graphs with one source and one sink of $\Omega (\log n/(\log\log n)^2)$ per operation. We give a lower bound of $\Omega\big(\surd(\log n/\log \log n)\big)$ for the dynamic membership problem of any Dyck language with two or more letters. This implies the same lower bound for the dynamic word problem for the free group with $k$ generators. We also give lower bounds for the dynamic prefix majority and prefix equality problems", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-8, author = "Hansen, Martin and H{\"u}ttel, Hans and Kleist, Josva", title = "Bisimulations for Asynchronous Mobile Processes", institution = brics, year = 1996, type = rs, number = "RS-96-8", address = iesd, month = apr, note = "18~pp. Abstract appears in BRICS Notes Series NS-94-6, pages 188--189. Appears in {\em Tbilisi Symposium on Language, Logic, and Computation} (Tbilisi, Republic of Georgia, October 19--22, 1995)", abstract = "Within the past few years there has been renewed interest in the study of value-passing process calculi as a consequence of the emergence of the $\pi$-calculus. Here, Milner et.\ al have determined two variants of the notion of {\em bisimulation}, {\em late} and {\em early} bisimilarity. Most recently Sangiorgi has proposed the new notion of {\em open} bisimulation equivalence.\bibpar In this paper we consider Plain LAL, a mobile process calculus which differs from the $\pi $-calculus in the sense that the communication of data values happens {\em asynchronously}. The surprising result is that in the presence of asynchrony, the open, late and early bisimulation equivalences {\em coincide} -- this in contrast to the $\pi$--calculus where they are distinct. The result allows us to formulate a common {\em equational theory} which is sound and complete for finite terms of Plain LAL.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-7, author = "Damg{\aa}rd, Ivan B. and Cramer, Ronald", title = "Linear Zero-Knowledge - {A} Note on Efficient Zero-Knowledge Proofs and Arguments", institution = brics, year = 1996, type = rs, number = "RS-96-7", address = daimi, month = apr, note = "17~pp. Appears in " # acmstoc97 # ", pages 436--445", abstract = "We present a zero-knowledge proof system for any NP language $L$, which allows showing that $x\in L$ with error probability less than $2^{-k}$ using communication corresponding to $O(|x|^c)+k$ {\em bit commitments}, where $c$ is a constant depending only on $L$. The proof can be based on any bit commitment scheme with a particular set of properties. We suggest an efficient implementation based on factoring.\bibpar We also present a 4-move perfect zero-knowledge interactive argument for any NP-language $L$. On input $x\in L$, the communication complexity is $O(|x|^c)\cdot max(k,l)$ {\em bits}, where $l$ is the security parameter for the prover (The meaning of $l$ is that if the prover is unable to solve an instance of a hard problem of size $l$ before the protocol is finished, he can cheat with probability at most $2^{-k}$). Again, the protocol can be based on any bit commitment scheme with a particular set of properties. We suggest efficient implementations based on discrete logarithms or factoring.\bibpar We present an application of our techniques to multiparty computations, allowing for example $t$ committed oblivious transfers with error probability $2^{-k}$ to be done simultaneously using $O(t+k)$ commitments. Results for general computations follow from this.\bibpar As a function of the security parameters, our protocols have the smallest known asymptotic communication complexity among general proofs or arguments for NP. Moreover, the constants involved are small enough for the protocols to be practical in a realistic situation: both protocols are based on a Boolean formula $\Phi$ containing and-, or- and not-operators which verifies an NP-witness of membership in $L$. Let $n$ be the number of times this formula reads an input variable. Then the communication complexity of the protocols when using our concrete commitment schemes can be more precisely stated as at most $4n+k+1$ commitments for the interactive proof and at most $5nl +5l$ bits for the argument (assuming $k\leq l$). Thus, if we use $k=n$, the number of commitments required for the proof is linear in $n$.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-6, author = "Goldberg, Mayer", title = "An Adequate Left-Associated Binary Numeral System in the $\lambda$-Calculus (Revised Version)", institution = brics, year = 1996, type = rs, number = "RS-96-6", address = daimi, month = mar, note = "19~pp. Appears in {\em Journal of Functional Programming} 10(6):607--623, 2000. This report is a revision of the BRICS Report~RS-95-42", abstract = "This paper introduces a sequence of $\lambda $-expressions modelling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system. These functions can be computed efficiently. Their complexity is independent of the order of evaluation", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-5, author = "Goldberg, Mayer", title = "G{\"o}delisation in the $\lambda$-Calculus (Extended Version)", institution = brics, year = 1996, type = rs, number = "RS-96-5", address = daimi, month = mar, note = "10~pp Appears in {\em Information Processing Letters} 75(1--2):13--16, 2000. Earlier version " # alsoasrs # "RS-95-38", keywords = "Programming Calculi; $\lambda$-Calculus; G{\"o}delisation.", abstract = "G{\"o}delisation is a meta-linguistic encoding of terms in a language. While it is impossible to define an operator in the $\lambda$-calculus which encodes all closed $\lambda$-expressions, it is possible to construct restricted versions of such an encoding operator modulo normalisation. In this paper, we propose such an encoding operator for proper combinators", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-4, author = "Andersen, J{\o}rgen H. and Harcourt, Ed and Prasad, K. V. S.", title = "A Machine Verified Distributed Sorting Algorithm", institution = brics, year = 1996, type = rs, number = "RS-96-4", address = iesd, month = feb, note = "21~pp. Abstract appeared in " # nwpt7 # ", pages 62--82", abstract = "We present a verification of a distributed sorting algorithm in ALF, an implementation of Martin L{\"o}f's type theory. The implementation is expressed as a program in a priortized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey--Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-3, author = "van Oosten, Jaap", title = "The Modified Realizability Topos", institution = brics, year = 1996, type = rs, number = "RS-96-3", address = daimi, month = feb, note = "17~pp. Appears in {\em Journal of Pure and Applied Algebra}, 116:273--289, 1997 (the special Freyd issue)", abstract = "The modified realizability topos is the semantic (and higher order) counterpart of a variant of Kreisel's modified realizability (1957). These years, this realizability has been in the limelight again because of its possibilities for modelling type theory (Streicher, Hyland-Ong-Ritter) and strong normalization.\bibpar In this paper this topos is investigated from a general logical and topos-theoretic point of view. It is shown that Mod (as we call the topos) is the {\em closed complement\/} of the effective topos inside another one; this turns out to have some logical consequences. Some important subcategories of Mod are described, and a general logical principle is derived, which holds in the larger topos and implies the well-known Independence of Premiss principle.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-2, author = "Cheng, Allan and Nielsen, Mogens", title = "Open Maps, Behavioural Equivalences, and Congruences", institution = brics, year = 1996, type = rs, number = "RS-96-2", address = daimi, month = jan, note = "25~pp. A short version of this paper appeared in " # lncs1059 # ", pages 257--272, and a full version appears in {\em Theoretical Computer Science}, 190(1):87--112, " # jan # " 1998", abstract = "Spans of open maps have been proposed by Joyal, Nielsen, and Winskel as a way of adjoining an abstract equivalence, ${\cal P}$-bisimilarity, to a category of models of computation ${\cal M}$, where ${\cal P}$ is an arbitrary subcategory of observations. Part of the motivation was to recast and generalise Milner's well-known strong bisimulation in this categorical setting. An issue left open was the {\em congruence properties\/} of ${\cal P}$-bisimilarity. We address the following fundamental question: given a category of models of computation ${\cal M}$ and a category of observations ${\cal P}$, are there any conditions under which algebraic constructs viewed as functors preserve ${\cal P}$-bisimilarity? We define the notion of functors being {\em${\cal P}$-factorisable}, show how this ensures that ${\cal P}$-bisimilarity is a congruence with respect to such functors. Guided by the definition of ${\cal P}$-factorisability we show how it is possible to parametrise proofs of functors being ${\cal P}$-factorisable with respect to the category of observations ${\cal P}$, i.e., with respect to a behavioural equivalence.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-96-1, author = "Brodal, Gerth St{\o}lting and Husfeldt, Thore", title = "A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth", institution = brics, year = 1996, type = rs, number = "RS-96-1", address = daimi, month = jan, note = "3~pp", abstract = "We present a direct protocol with logarithmic communication that finds an element in the symmetric difference of two sets of different size. This yields a simple proof that symmetric functions have logarithmic circuit depth.", linkhtmlabs = "", linkdvi = "", linkps = "" }