## On a symbolic method of verification for definite iteration over data structures

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...

## Reachability analysis for time Petri nets without overlappings of firing intervals

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...

## Simple semantic analysis problems for functional programs

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

## Correct transformations of logic programs

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...

## Agents as constraint objects

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...

## An algebra of labelled nondeterministic processes

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...

## Equivalence notions for event structures and refinement of actions

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...