International Journal of Foundations of Computer Science

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

A temporal logic of causality (TLC) was introduced by Alur, Penczek, and Peled in [1]. It is basically a linear time temporal logic interpreted over Mazurkiewicz traces which allows quantification over causal chains. Through this device one can directly formulate causality properties of distributed systems. In this paper we consider an extension of TLC by strengthening the chain quantification operators. We show that our logic TLC* adds to the expressive power of TLC. We doso by defining an Ehrenfeucht-Fraïssé game to capture the expressive power of TLC. We then exhibit a property and by means of this game prove that the chosen property is not definable in TLC. We then show that the same property is definable in TLC*. We prove in fact the stronger result that TLC* is expressively stronger than TLC exactly when the dependency relation associated with the underlying trace alphabet is not transitive. We then show that TLC* defines only regular trace languages by embedding it into the monadic second-order logic. Finally, the relative expressive power of TLC* and similar logics for traces is compared.

Inductive proofs are commonly used in automated deduction systems or functional programming, such as for instance the ProPre system, for establishing the termination of recursively defined functions. Such proofs deal with the structural orderings of the term algebras that define the domain of the functions. However there exists other interesting functions whose termination requires different underlying orderings. To treat a class of such functions that are not taken into account by systems such as ProPre, we develop termination properties that can be shown automatically. In contrast with the ProPre system that builds formal trees based on inductive proofs, we generate measures that satisfy an extended termination property and well-founded orderings which ensure the termination of the functions.

Unfold/fold transformation systems for logic programs have been extensively investigated. Existing unfold/fold transformation systems for normal logic programs typically fold using a single, non-recursive clause i.e. the folding transformation is very restricted. In this paper we present a transformation system that permits folding in the presence of recursion, disjunction, as well as negation. We show that the transformations are correct with respect to various model theoretic semantics of normal logic programs including the well-founded model and stable model semantics.

We study the problem of resizing gates so as to reduce overall power consumption while satisfying a circuit's timing constraints. Polynomial time algorithms for series-parallel and tree circuits are obtained. Gate resizing with multigate modules is shown to be NP-hard. Algorithms that improve upon those presented by Chen and Sarrafzadeh⁴ for general circuits are also developed.

An algorithm M is described that solves any well-defined problem p as quickly a the fastest algorithm computing a solution to p, save for a factor of 5 and low-order additive terms. M optimally distributes resources between the execution of provably correct p-solving programs and an enumeration of all proofs, including relevant proofs of program correctness and of time bounds on program runtimes. M avoids Blum's speed-up theorem by ignoring programs without correctness proof. M has broader applicability and can be faster than Levin's universal search, the fastest method for inverting functions save for a large multiplicative constant. An extension of Kolmogorov complexity and two novel natural measures of function complexity are used to show the most efficient program computing some function f is also among the shortest programs provably computing f.

Decision tables provide a natural framework for knowledge acquisition and representation in the area of knowledge based information systems. Decision trees provide a standard method for inductive inference in the area of machine learning. In this paper we show how decision tables can be considered as ordered decision trees: decision trees satisfying an ordering restriction on the nodes. Every decision tree can be represented by an equivalent ordered decision tree, but we show that doing so may exponentially blow up sizes, even if the choice of the order is left free.

Our main result states that finding an ordered decision tree of minimal size that represents the same function as a given ordered decision tree is an NP-hard problem; in earlier work we obtained a similar result for unordered decision trees.

We consider the problem of labeling a directed multigraph so that it becomes a synchronized finite automaton, as an ultimate goal to solve the famous Road Coloring Conjecture, cf. [1,2]. We introduce a relabeling method which can be used for a large class of automata to improve their 'degree of synchronization'. This allows, for example, to formulate the conjecture in several equivalent ways.