Jaana Eloranta: Minimal transition systems with respect to divergence preserving behavioural equivalences. A-1994-1.
Three divergence preserving behavioural equivalences for labelled transition systems (lts), namely D-bisimilarity, branching D-bisimilarity and CFFD-equivalence, are analyzed and compared. For an image-finite lts, which does not contain an infinite sequence of distinct t-connected states, it is possible to find the unique lts which is state- and transition-minimal with respect to D-bisimilarity or branching D-bisimilarity. It is well known how to find an equivalent state-minimal lts. We show how the state and transition-minimal lts can be found, and moreover give a transition minimization algorithm in a finite case. In the case of CFFD-equivalence, which is a modification of failures-equivalence, a unique state- and transition-minimal lts cannot always be found.
For rooted versions of D-bisimilarity and branching D-bisimilarity the uniqueness result holds only for root-unwound lts's. Related equivalences, D-congruence and branching D-congruence, handle the first transitions from a root, rather than a root itself, in a special way. The relation between rooted equivalences and corresponding congruences is fully analyzed. For D-congruence and branching D-congruence a unique root-unwound minimal lts is found, for an image-finite (without an infinite sequence of distinct t-connected states). Moreover, D-congruence and branching D-congruence are compositional with respect to Basic LOTOS operations. Since the same result holds for CFFD-equivalence, D-congruence, branching D-congruence and CFFD-equivalence are compatible with compositional reduction.
In order to apply and demonstrate the theoretical results, we specify and verify several concurrent systems. The specifications are reduced with respect to several equivalences, including D-congruence, branching D-congruence and CFFD-equivalence. The analysis shows that it is possible to find errors, as well as reasons for divergences by studying reduced lts's. Moreover, these case studies are used to test the effect of the transition-minimization algorithm, to compare divergence preserving and divergence ignoring equivalences, and to compare branching and weak versions of equivalences. In some studies compositional reduction is used and the results are analyzed. Furthermore, based on the results of these applications, we propose some modifications to the reduction algorithm with respect to CFFD-equivalence.
Petri Myllymäki: Mapping Bayesian networks to stochastic neural networks: a foundation for hybrid Bayesian-neural systems. A-1995-1.
In this work, we are interested in the problem of finding maximum a posteriori probability (MAP) value assignments for a set of discrete attributes, given the constraint that some of the attributes are permanently fixed to some values a priori. For building a system capable of this type of uncertain reasoning in practice, we need first to construct an accurate abstract representation of the problem domain, and then to establish an efficient search mechanism for finding MAP configurations within the constructed model. We propose a hybrid Bayesian network-neural network system for solving these two subtasks. The Bayesian network component can be used for constructing a compact, high-level representation for the problem domain probability distribution quickly and reliably, assuming that suitable expert knowledge is available. The neural network component provides then a computationally efficient, massively parallel platform for searching the model state space. The main application areas for these kinds of systems include configuration and design problems, medical diagnosing and pattern recognition.
For implementing a hybrid Bayesian-neural system as suggested above, we present here methods for mapping a given Bayesian network to a stochastic neural network architecture, in the sense that the resulting neural network updating process provably converges to a state which can be projected to a MAP state on the probability distribution corresponding to the original Bayesian network. From the neural network point of view, these mappings can be seen as a method for incorporating high-level, probabilistic a priori information directly into neural networks, without recourse to a time-consuming and unreliable learning process. From the Bayesian network point of view, the mappings offer a massively parallel implementation of simulated annealing where all the variables can be updated at the same time. Our empirical simulations suggest that this type of massively parallel simulated annealing outperforms the traditional sequential Gibbs sampling/simulated annealing process, provided that suitable hardware is available.
Roope Kaivola: Equivalences, preorders and compositional verification for linear time temporal logic and concurrent systems. A-1996-1.
A promising approach to formal specification and verification of finite-state concurrent systems is using propositional temporal logic as a specification language and applying automated model-checking algorithms for the verification task. However, the so-called state explosion-problem caused by representing concurrency by interleaving makes model-checking in many cases practically intractable. One way of attacking this problem is replacing the modules of a system by smaller ones so that the visible properties of the system are not affected. This approach leads to notions of compositional property-preserving equivalences and preorders between modules.
This work examines the uses of equivalences and preorders in verifying nexttime-less linear temporal logic properties. Concurrent systems are modelled here by labelled transition systems augmented with state information, and both synchronization and read-shared variables are considered as methods of communication. We examine a novel equivalence notion, called the non-divergent failures divergences or NDFD-equivalence. It is shown that NDFD preserves all nexttime-less linear temporal logic properties, and that it is compositional with respect to parallel composition and abstraction by hiding and encapsulation. Conversely, it is shown that NDFD is the weakest such equivalence, i.e. that it is fully abstract with respect to preserving nexttime-less linear temporal logic properties in an arbitrary context. The computational complexity of determining NDFD-equivalence is also examined and the problem is shown to be PSPACE-complete.
Analogous to NDFD-equivalence, the theory of NDFD-preorder is developed and the compositionality, full abstractness and computational complexity results extended to it. Moreover, it is shown that the verification technique of modular validity introduced by Manna and Pnueli corresponds to an extremal case of NDFD-preorder. As a larger case study illustrating the practical applications of the results, we use the NDFD-preorder to verify semi-automatically both safety and liveness properties of the sliding window communication protocol for arbitrary channel lengths and realistic parameter values. In this process we locate a previously undiscovered fault leading to lack of liveness in a version of the protocol.
Tapio Elomaa: Tools and techniques for decision tree learning. A-1996-2.
Decision tree learning is an important field of machine learning. In this study we examine both formal and practical aspects of decision tree\ learning. We aim at answering to two important needs: The need for better motivated decision tree learners and an environment facilitating experimentation with inductive learning algorithms. As results we obtain new practical tools and useful techniques for decision tree learning.
First, we derive the practical decision tree learner Rank based on the Findmin protocol of Ehrenfeucht and Haussler. The motivation for the changes introduced to the method comes from empirical experience, but we prove the correctness of the modifications in the probably approximately correct learning framework. The algorithm is enhanced by extending it to operate in the multiclass situations, making it capable of working within the incremental setting, and providing noise tolerance into it. Together these modifications entail practicability through a formal development process, which constitutes an important technique for decision tree\ learner design.
The other tool that comes out of this work is TELA, a general testbed for all inductive learners using attribute representation of data, not only for decision tree learners. This system guides and assists its user in taking new algorithms to his disposal, operating them in an easy fashion, designing and executing useful tests with the algorithms, and in interpreting the outcome of the tests. We present the design rationale, current composition, and future development directions of TELA. Moreover, we reflect on the experiences that have been gathered in the initial usage of the system.
The tools that come about are evaluated and validated in empirical tests over many real-world application domains. Several successful inductive algorithms are contrasted with the Rank algorithm in experiments that are carried out using TELA. These experiments let us evaluate the success of the new decision tree learner with respect to its established equivalents and validate the utility of the developed testbed. The tests prove successful in both respects: Rank attains the same overall level of prediction accuracy as C4.5, which is generally considered to be one of the best empirical decision tree learners, and TELA eases the execution of the experiments substantially.