Fundamenta Informaticae

Resources are defined as submultisets of Petri net markings. Two resources are called similar if replacing one of them by another in any marking doesn't change the Petri net's behavior. We define the relations of resource similarity and resource bisimulation and show that they are finitely based. In this paper the resource bisimulation is studied for different classes of Petri nets: ordinary Petri nets, high-level Petri nets and nested Petri nets — Petri nets with Petri nets as tokens.

MGU_{mon} and MGU_{k-rep} have a complementary role in unification in the complexity class NC. MGU_mon is the upper bound of the unification classes that fall in NC and whose inputs admit an unrestricted number of repeated variables. MGU_{k-rep} is the upper bound of the unification classes that still fall in NC but whose inputs admit an unrestricted arity on term constructors. No LogSpace reduction of the one to the other class is known. Moreover, very fast algorithms that solve the two separately are well known but no one is able to compute with both in polylog PRAM-Time. N-axioms unification extends the structure of unification inputs and brings out the notion of interleaving variable as a special repeated variable which serializes independet computations. Based on it, we define the unification class AMGU^k_{p/h} whose inputs have a fixed number of interleaving variables but admit unrestricted number of repeated variables and, at the same time, unrestricted arity for term constructors. Constructively, we prove that AMGU^k_{p/h} is in NC by introducing a new unification algorithm that works on graph contractions and solves AMGU^k_{p/h} in a polylog PRAM time of the input size. Finally, we prove that MGU_{mon}, MGU_{k-rep} , and MGU_{linear} all are LogSpace reducible to AMGU^k_{p/h}. Hence, AMGU^k_{p/h} becomes the upper bound of the unification classes that are proved to be in NC.

Fehling's hierarchical Petri nets are a net modelling framework based on refinement and abstraction of nets. Object Petri nets are a Petri net-based method of encapsulation. We bring these two domains together in the new concept of hierarchical object Petri nets. Defining hierarchical object Petri nets forces us to consider what it means to preserve synchronisation when abstracting or refining an object Petri net. The goal is to provide a sound theoretical basis for building computer tools to develop high-level Petri net models following the nets-within-nets paradigm.

The synthesis problem of concurrent data models from experimental tables based on rough set approach has earlier been discussed [14], [15] Classical Petri nets have been used as a model for concurrency. In this paper we propose the nets with inhibitor expressions and Coloured Petri Nets as models for concurrency. The nets with inhibitor expressions are defined on the base of so called inhibitor rules extracted from modelled systems. The approach presented in this paper enables to implement the algorithms for easier construction of Petri net models. The proposed approach can be applied to discover data models in semi-automatic way. The obtained models enable us to determine all global states of a modelled system represented by an information system, consistent with all rules extracted from the given information system.

We present a framework for verifying temporal and epistemic properties of multi-agent systems by means of bounded model checking. We use interpreted systems as underlying semantics. We give details of the proposed technique, and show how it can be applied to the "attacking generals problem", a typical example of coordination in multi-agent systems.

Non-reachability proofs in Timed Petrinets were usually done by proving the non-reachability within the underlying timeless net. However, in many cases this approach fails. In this paper, we present an approach to prove non-reachability within the actual Timed Petrinet. For this purpose, we introduce a state equation for Timed Petrinets in analogy to timeless nets. Using this state equation, we can express reachability as a system of equations and inequations, which is solvable in polynomial time.

The paper presents a new method for checking reachability properties of Timed Automata. The idea consists in on-the-fly verification of a property on a pseudo-bisimulating model generated by a modified partitioning algorithm. Pseudo-bisimulating models are often much smaller than forward-reachability graphs commonly used in reachability analysis. A theoretical description of the algorithm is supported by several experimental results.

The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a~state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.