Computer Science, № 13, 2000

A new notion of a multi-branch narrowing that allows case analysis to be built in is introduced. A narrowing strategy that preserves formula satisfiability is suggested. A formalism called formula rewriting systems specifying the strategy is defined. The termination of formula rewriting systems is considered.

A pair consisting of a place and a token in a coloured Petri net is considered as an elementary resource for this net, and a resource is a multiset of elementary resources. Two resources are bisimilar, if replacement of one by another in any marking doesn't change the net behaviour...

Based on notions of computability for operators and real-valued functionals, a background for formalisation of complex systems is introduced. We propose a recursion scheme which is a suitable tool for formalisation of complex systems, such as hybrid systems. In this framework the trajectories of continuous parts of hybrid systems can...

The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow a restricted change of the structures by the iteration body and exit from the iteration body under a condition. A transformation of definite iterations which use exit from the iteration bodies to the standard definite...

The paper discusses some issues related to model checking utility and reliability: (1) utility of model checking and games for solving puzzles, and (2) importance of games and puzzles for validation of model checkers.

We consider the process algebra BPA* proposed by Bergstra, Bethke, and Ponse, since it nicely defines a class of infinite processes. Investigation of representation of event structures for this class of processes is presented in this article. We extend the algebra BPA* by a parallel composition and modify its sequential...

Dataflow networks are a well-known mathematical tool extensively used for representing, analyzing and modeling concurrent computing systems and their software. Formal dataflow models reported in the literature may be divided in two groups – static and dynamic. Static models admit at most one token on an arc. This assumption severely...

An important problem of the representation of a big dynamic system as a number of interrelating typed Gurevich Machines (Abstract State Machines or just ASMs in the sequel) and the subsequent combination of the specifications of individual ASMs into the specification of the whole system is investigated in the paper...