Computer Science, № 5, 1996

A verification method is proposed for definite iteration over different data structures. The method is based on a replacement operation, which expresses the definite iteration effect in a symbolic form and belongs to a specification language. The method includes a proof rule for the iteration without invariants and inductive proof...

This paper discusses a subclass of Merlin’s time Petri nets called here time Petri nets without overlappings of firing intervals. In addition to the existing enumerative procedure for time nets, a new technique of reachability analysis for nets in the subclass is presented. Correctness of the presented method is proved...

In the paper two problems of semantic property analysis of recursion schemes are stated and a marking technique for solving these problems is described.

This paper describes a system of transformations that preserves the semantics of logic programs with respect to a fixed goal. We formalise some standard transformations and introduce two new transformation rules: Copying/Merge of Copies and Contextual Replacement by Equal Term. Correctness of all schemes of the transformation rules is...

In the paper a multi-agent technology based on integration of the object- oriented approach and constraint programming is proposed. The key notion of this technology is an ’’active object” that has three specific features. First, an active object has the ability to change its state based on the analysis of...

A new calculus of labelled nondeterministic processes AFLP2 is proposed which is an extension of the known calculus AFP2 by labelling function. The denotational and operational semantics and complete axiomatization of the semantic equivalence are presented. The interrelation of net equivalences from with equivalences of the algebra (semantic...

We consider different equivalence notions for prime event structures, which explicitly reflect causality, concurrency and conflict relations between occurrences of events in the structures. The intention of the paper is to establish whether or not these equivalences are preserved under refinement of actions. An operator of refinement replaces actions on...