A multi-branch narrowing: satisfiability and termination
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.
Reduction of coloured Petri nets based on resource bisimulation
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...
Background for formalisation of complex systems
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...
Verification of pointer programs using symbolic method for definite iterations
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...
Model checking puzzles in μ-Calculus
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.
Algebraic characterization of behavioural equivalences over event structures
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...
Algebraic specifications for dataflow computations design
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...
Modularization of typed Gurevich machines
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...