Fundamenta Informaticae - Volume 80, issue 1-3

Article Type: Other

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. i-ii, 2007

Authors: Diekert, Volker | Horsch, Martin | Kufleitner, Manfred

Article Type: Research Article

Abstract: Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments. One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids calledDA. However, overMazurkiewicz traces it is …crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known. This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE. Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power. Show more

Keywords: Mazurkiewicz traces, temporal logic, first-order logic, Ehrenfeucht-Fraïssé games

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 1-29, 2007

Authors: Bernardinello, Luca | Monticelli, Elena | Pomello, Lucia

Article Type: Research Article

Abstract: We study several properties of an operation which combines two net systems by identifying local states and synchronizing events according to morphisms towards an interface. We propose this operation as a tool for modular system design, where different components are required to comply with a shared interface, or protocol of communication. We prove results on the preservation of structural properties, expressed as invariants, and of behavioural properties, in particular of deadlock-freeness.

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 31-47, 2007

Authors: Billington, Jonathan | Han, Bing

Article Type: Research Article

Abstract: The TCP/IP protocol suite defines the procedures governing the movement of data within the Internet. A major component of the suite is the Transmission Control Protocol (TCP), which ensures data flows reliably between Internet applications. We use Coloured Petri Nets (CPNs) to model the application's view of the service provided by TCP for the transfer of data. This service depends on the storage capacity available in the Internet. We firstly establish exact expressions for the size …of the CPN model's reachability graph (or state space) in terms of the storage capacity. They indicate that both the nodes and arcs of the state space grow exponentially in the storage capacity. Secondly,we derive a symbolic state space which represents an infinite family of state spaces, one for each value of the capacity. We prove that each member of this family is a strongly connected graph and that its associated finite state automaton is deterministic and minimum. Finally, we formulate the TCP data transfer service language for arbitrary capacity, from the symbolic representation of the family of automata. This service language is the yardstick against which the TCP data transfer protocol can be verified with respect to user observable sequences of events. Show more

Keywords: TCP, Data Transfer Service, Service Language, Parametric Systems, Symbolic Automata, Coloured Petri Nets

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 49-74, 2007

Authors: Best, Eike | Darondeau, Philippe | Wimmel, Harro

Article Type: Research Article

Abstract: This paper discusses the following results: that bounded Petri nets can be transformed into pomset-equivalent safe nets; that boundedmarked graphs can be transformed into step-language-equivalent safe marked graphs; that safe labelled marked graphs can be transformed into τ–free safe labelled marked graphs; and that marked graphs can be separated. The paper also lists some open problems that have arisen in this context.

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 75-90, 2007

Authors: Conforti, Giovanni | Macedonio, Damiano | Sassone, Vladimiro

Article Type: Research Article

Abstract: Aiming at a unified view of the logics describing spatial structures, we introduce a general framework, BiLog, whose formulae characterise monoidal categories. As a first instance of the framework we consider bigraphs, which are emerging as a an interesting (meta-)model for spatial structures and distributed calculi. Since bigraphs are built orthogonally on two structures, a hierarchical place graph for locations and a link (hyper-)graph for connections, we obtain a logic that is a natural …composition of other two instances of BiLog: a Place Graph Logic and a Link Graph Logic. We prove that these instances generalise the spatial logics for trees, for graphs and for tree contexts. We also explore the concepts of separation and sharing in these logics. We note that both the operator ∣ of Separation Logic and the operator * of spatial logics do not completely separate the underlying structures. These two different forms of separation can be naturally derived as instances of BiLog by using the complete separation induced by the tensor product of monoidal categories along with some form of sharing. Show more

Keywords: Bigraphs, Spatial Logics, Context Logic, Separation

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 91-110, 2007

Authors: Engelfriet, Joost | Hoogeboom, Hendrik Jan

Article Type: Research Article

Abstract: The hierarchy of arbitrary compositions of two-way nondeterministic finite-state transductions collapses when restricted to finitary transductions, i.e., transductions that produce a finite set of outputs for each input. The hierarchy collapses to the class of nondeterministic MSO definable transductions, which is inside the second level of that hierarchy. It is decidable whether a composition of two-way nondeterministic finite-state transducers realizes a finitary transduction (i.e., is MSO definable).

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 111-123, 2007

Authors: Carette, Jacques | Janicki, Ryszard

Article Type: Research Article

Abstract: We show how properties of an interesting class of imperative programs can be calculated by means of relational modeling and symbolic computation. The ideas of [5, 26] are implemented using symbolic computations based on Maple [30].

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 125-146, 2007

Authors: Genest, Blaise | Kuske, Dietrich | Muscholl, Anca

Article Type: Research Article

Abstract: We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.

Keywords: Communicating automata, Mazurkiewicz traces

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 147-167, 2007

Authors: Gastin, Paul | Kuske, Dietrich

Article Type: Research Article

Abstract: We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 169-197, 2007

Authors: Kleijn, Jetty | Koutny, Maciej

Article Type: Research Article

Abstract: We are concerned with causality semantics in the executions of Petri nets with range arcs. Range arcs combine (and subsume) the distinctive features of inhibitor and activator arcs, and each such arc provides a means of specifying a range (a finite or infinite interval of non-negative integers) for the number of tokens in a place which makes enabling of a given transition possible. We demonstrate that the existing treatment of causality developed for Petri nets with …inhibitor arcs based on structures generalising partial orders can also be applied to nets with range arcs. Show more

Keywords: theory of concurrency, Petri nets, weighted activator and inhibitor arcs, range arcs, causality semantics, infinite processes, occurrence nets, step sequences

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 199-219, 2007

Authors: Chalopin, Jérémie | Métivier, Yves

Article Type: Research Article

Abstract: We study the election and the naming problems in the asynchronous message passing model. We present a necessary condition based on Angluin's lifting lemma [1] that must be satisfied by any network that admits a naming (or an election) algorithm. We then show that this necessary condition is also sufficient: we present an election and naming algorithm based on Mazurkiewicz's algorithm [17]. The algorithmwe obtained is totally asynchronous and it needs a polynomial number of messages …of polynomial size, whereas previous election algorithms in this model are pseudosynchronous and use messages of exponential size. Show more

Keywords: Distributed Algorithm, AsynchronousMessage Passing Model, Anonymous Network, Local Computation, Election, Naming, Covering

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 221-246, 2007

Authors: Moshkov, Mikhail Ju. | Skowron, Andrzej | Suraj, Zbigniew

Article Type: Research Article

Abstract: The minimal rules for information systems are often used for inducing data models by methods in which the optimization of models is based on the minimal length principle. We show that almost all information systems from a certain large class of information systems have relatively short minimal rules. However, the number of such rules is not polynomial in the number of attributes and the number of objects. This class consists of all binary information systems with …the number of objects polynomial in the number of attributes. Hence, for efficient inducing data models some filtration techniques in rule generation are necessary. In our further study we would like to extend our results for arbitrary information systems. Show more

Keywords: Information systems, minimal rules, irreducible inconsistent systems of equations

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 247-258, 2007

Authors: Ochmański, Edward | Pieckowska, Joanna

Article Type: Research Article

Abstract: We extend the well-known hierarchy ∞-fair ⊆ 0-fair ⊆ just for sequences (sequential computations) to that of traces (concurrent processes). The fairness hierarchy for traces is similar, but more involved than for sequences. We study this hierarchy, first in general, abstracting from concrete concurrent system, then for basic classes of Petri nets – elementary and place/transition nets. Finally, we define the fairness notions in a non-interleaving way and compare them with the former ones.

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 259-272, 2007

Authors: Reisig, Wolfgang

Article Type: Research Article

Abstract: Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 273-281, 2007

Authors: Wang, Xu | Kwiatkowska, Marta

Article Type: Research Article

Abstract: Asynchronous circuits have received much attention recently due to their potential for energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis of asynchronous circuits. This paper develops a theoretical basis for using process algebra and associated model checking tools to verify asynchronous circuits. We formulate a model that extends existing verification theory for asynchronous circuits, and integrate it into the framework of standard process algebra theory. Our theory permits …analysis of safeness (i.e. choke) and progress (i.e. illegal stop, divergence and relative starvation) conditions. We show how the model can be translated into CSP, and how the satisfaction of safeness and progress requirements can be reduced to refinement checks in CSP. Finally, the correspondence of our theory with trace theory (i.e. prefix-closed trace structures), receptive process theory and the XDI model is investigated. Show more

Keywords: Process algebra, asynchronous circuits, assume/guarantee verification, progress/liveness, and CSP/FDR2

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 283-310, 2007

Authors: Winkowski, Józef

Article Type: Research Article

Abstract: The paper is devoted to characterizing hybrid systems by specifying their possible runs, called processes, where each process is represented by a pomset in an intrinsic, global time independent way and can possibly be obtained by composing sequentially and in parallel other processes.

Keywords: Hybrid systems, processes, states, sequential composition, parallel composition, category, partial monoid, structure, random behaviour

Citation: Fundamenta Informaticae, vol. 80, no. 1-3, pp. 311-332, 2007