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