Composantes préconservatives minimales d'un réseau de Petri : étude structurelle
Composition/décomposition de réseaux de Pétri et de leurs graphes de couverture
Concurrently controlled grammars
This paper introduces a new variant of Petri net controlled grammars, namely a concurrently controlled grammar, where the control over the application of the productions of a grammar is realized by a Petri net with different parallel firing strategies. The generative capacity of these grammars is investigated with respect to transition labeling strategies, definitions of final marking sets and parallel transition firing modes. It is shown that the labeling strategies do not effect the computational...
Construction of very hard functions for multiparty communication complexity
Construction of Very Hard Functions for Multiparty Communication Complexity
We consider the multiparty communication model defined in [4] using the formalism from [8]. First, we correct an inaccuracy in the proof of the fundamental result of [6] providing a lower bound on the nondeterministic communication complexity of a function. Then we construct several very hard functions, i.e., functions such that those as well as their complements have the worst possible nondeterministic communication complexity. The problem to find a particular very hard function was...
Covering space theory for directed topology.
Decidability questions for some dynamic properties of Petri nets [Abstract of thesis]
Deciding knowledge in security protocols under some e-voting theories
In the last decade, formal methods have proved their interest when analyzing security protocols. Security protocols require in particular to reason about the attacker knowledge. Two standard notions are often considered in formal approaches: deducibility and indistinguishability relations. The first notion states whether an attacker can learn the value of a secret, while the latter states whether an attacker can notice some difference between protocol runs with different values of the secret. Several...
Deciding knowledge in security protocols under some e-voting theories
In the last decade, formal methods have proved their interest when analyzing security protocols. Security protocols require in particular to reason about the attacker knowledge. Two standard notions are often considered in formal approaches: deducibility and indistinguishability relations. The first notion states whether an attacker can learn the value of a secret, while the latter states whether an attacker can notice some difference between protocol runs with different values of the secret. Several...
Detection of deadlocks and traps in Petri nets by means of Thelen's prime implicant method
A new method of detecting deadlocks and traps in Petri nets is presented. Deadlocks and traps in Petri nets can be represented by the roots of special equations in CNF form. Such equations can be solved by using the search tree algorithm proposed by Thelen. In order to decrease the tree size and to accelerate the computations, some heuristics for Thelen's method are presented.
Fairness and regularity for SCCS processes
Formal Methods to Improve Public Administration Business Processes
Starting from late 90’s the public administration has started to employ a quite relevant amount of its budget in developing ICT solutions to better deliver services to citizens. In spite of this effort many statistics show that the mere availability of ICT based services does not guarantee per se their usage. Citizens have continued to largely access services through “traditional” means. In our study we suggest that the highlighted situation is partly due to the fact that relevant domain dependent...
Formal Methods to Improve Public Administration Business Processes
Starting from late 90’s the public administration has started to employ a quite relevant amount of its budget in developing ICT solutions to better deliver services to citizens. In spite of this effort many statistics show that the mere availability of ICT based services does not guarantee per se their usage. Citizens have continued to largely access services through “traditional” means. In our study we suggest that the highlighted situation is partly...
Formulation of Cell Petri Nets
Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...
FSP and FLTL framework for specification and verification of middle-agents
Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers....
Fuites dans les réseaux de Petri
Generalized Nets Model of an E-Learning System Software Architecture
The paper has been presented at the International Conference Pioneers of Bulgarian Mathematics, Dedicated to Nikola Obreshko ff and Lubomir Tschakaloff , Sofi a, July, 2006.Component-based software engineering and software architecture are tightly connected areas in computer science. Software architecture presents the functionality of the system as decomposition into components, the properties of these components and the connectors between them. This paper illustrates a methodology for application...
Generic commutative separable algebras and cospans of graphs.
Geometrical characterization of observability in Interpreted Petri Nets
This work is concerned with observability in Discrete Event Systems (DES) modeled by Interpreted Petri Nets (IPN). Three major contributions are presented. First, a novel geometric characterization of observability based on input-output equivalence relations on the marking sequences sets is presented. Later, to show that this characterization is well posed, it is applied to linear continuous systems, leading to classical characterizations of observability for continuous systems. Finally, this paper...
Globular realization and cubical underlying homotopy type of time flow of process algebra.