Introduce heuristically the newly definitioll (W. Thomas) for graph automata - using"tiles" to simulste the extension (over dag's) of the classical notions of transition moves; proposea sufficient condition for when graph automata can be reduced to (simpler) tiling systerms, whichis a generalisation of a Thomas' result; and finally study the logic sepcification of tiling systems(paticularly, over picture languages) by (existential) monadic partition logic, instead of theususal and stronger framework (E)MSQ.

An extension of the simply-typed lambda calculus with constructs for expressing a notioncalled underdeterminism is studied. This allows us to interpret notions of stub and skeletonused in top-down program development. We axiomatise a simple notion of program refinement,and give a semantics, for which the calculus is proved sound and complete.

The paper proposes reaction graphs as graphical representations of computational objects.A reaction graph is a directed graph with all its arrows and some of its nodes labeled. Compu-tations are modeled by graph rewriting of a simple nature. The basic rewriting rules embodythe essence of both the communications among processes and cut-eliminations in proofs. Cal-culi of graphs are identified to give a formal and algebraic account of reaction graphs in thespirit of process algebra. With the help of the calcu…

We present a new testing semantics, called friendly testing, whose main property is thatthe induced preorder between processes fr is consistent with the conformance relation, andso we have, for instance, a b fr a fr a + b. The new theory is strongly based on De Nicola& Hennessy's work on testing. Friendly tests are defined exactly as in their work, except thatinternal actions are not allowed. However, in order to obtain the desired notion of friendlytesting this restriction is not enough and we also have to…

In this paper the definition of order-sorted algebra is generalized by introducing transforma-tion functions between subtypes and supertypes. According to our definition, a type needn'tbe a subset of its supertype and a record model may form an order-sorted algebra. A newdefinition of equation is given. It has also been proved that equational theories and describingsingle inheritance have the initial model.

In this paper, we derive, by presenting some suitable notations, three typical graph aLgorithms and corresponding programs using a unified approach, partition-and-recur. We putemphasis on the derivation rather than the algorithms themselves. The main ideas and lugesnutty of these algorithms are revealed by formula deduction. Success in these examples givesus more evidence that partition-and-recur is a simple and practical approach and developingenough suitable notations is the key in designing and deriving …

Dependent type systems are the basis of many proof development environments. In Aspinalland Compagnoni's paper, a system λP≤ is proposed as a subtyping extension of the first orderdependent type system λP (also called An). λP≤ has nice meta-theoretic properties includingsubject reduction and decidability. In this article, v,e give a reformulation of λP≤ t called λII≤.The advantages of λII< include: type level transitivity elimination property and pretypesbasedsubtyping system. These features considerably fa…

Encodings in polymorphism with finite product types are considered. These encodings aregiven in terms of I-algebras. They have the property that the ground terms are precisely theclosed normal terms of the encoded types. The proof of a well-known result is transplantedto the setting and it is shown why weak recursion is admissible. The paper also shows how tocarry out the dual encodingS using the existential quantifier.

In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equiv...

A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used…

The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances respectively. Therefore, to get the better performance onall kinds of problems, SAT solver should know how to select different algorithms according tothe feature of instances. In this paper the differences of several effective SAT algorithms areanalyzed and two new parameters gb and & are proposed…

In disciplined Ada software development and maintenance, an adequate and suitable graphical representation for concurrency is important. To describe rendezvous ordering, tasking andexecuting flow of tasks, p graph--Rendezvous Ordering Graph is presenced in this paper. pgraph is a kind of-hierarchical oriented graph with nodes representing rendezvouses and edgesshowing'ordering relations between rendezvouses as well as flow of tasks. It can be used insoftware understanding, design description and documentati…