PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników
Powiadomienia systemowe
  • Sesja wygasła!

Znaleziono wyników: 15

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote On Conditions for Modular Verification in Systems of Synchronising Components
Drábik P., Maggiolo-Schettini A., Milazzo P.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 3/4
259-274
EN
Property preservation is investigated as an approach to modular verification, leading to reduction of the property verification time for formal models. For modelling purposes, formalisms with multi-way synchronisations are considered. For the modular verification technique to work, a specific type of synchronisation is required for which a sufficient and necessary condition is identified. It is a requirement on the semantics of the formalism, which is restricted to permit simultaneous execution only of component moves that make reference to each other. Implications for modular verification of several well-known formalisms for concurrent systems are investigated.
2
Content available remote A Notion of Biological Diagnosability Inspired by the Notion of Opacity in Systems Security
Barbuti R., Maggiolo-Schettini A., Milazzo P., Gruska D.P.
Fundamenta Informaticae
|
2010
|
Vol. 102, nr 1
19-34
EN
A formal model for diagnostics of biological systems modelled as P systems is presented. We assume the presence of some biologically motivated changes (frequently pathological) in the systems behavior and investigate when these changes could be diagnosed by an external observer by exploiting some techniques originally developed for reasoning on system security.
3
Content available remote A Formalism for the Description of Protein Interaction Dedicated to Jerzy Tiuryn on the Occasion of His Sixty Birthday
Barbuti R., Dezani-Ciancaglini M., Maggiolo-Schettini A., Milazzo P., Troina A.
Fundamenta Informaticae
|
2010
|
Vol. 103, nr 1-4
1-29
EN
The Calculus of Looping Sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus by labelling elements of sequences. Since two elements with the same label are considered to be linked, this allows us to represent protein interaction at the domain level. Well-formedness of terms are ensured by both a syntactic constraint and a type system: we discuss the differences between these approaches through the description of a biological system, namely the EGF pathway.
4
Content available remote Timed P Automata
Barbuti R., Maggiolo-Schettini A., Milazzo P., Tesei L.
Fundamenta Informaticae
|
2009
|
Vol. 94, nr 1
1-19
EN
To study systems whose dynamics changes with time, an extension of timed P systems is introduced in which evolution rules may vary with time. The proposed model is a timed automaton with a discrete time domain and in which each state is a timed P system. A result on expressive power and on features of the formalism sufficient for full expressiveness is proved and, as an application example, the model of an ecological system is given.
5
Content available remote P Systems with Transport and Diffusion Membrane Channels
Barbuti R., Maggiolo-Schettini A., Milazzo P., Tini S.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
17-31
EN
P Systems are computing devices inspired by the structure and the functioning of a living cell. A P System consists of a hierarchy of membranes, each of them containing a multiset of objects, a set of evolution rules, and possibly other membranes. Evolution rules are applied to the objects of the same membrane with maximal parallelism. In this paper we present an extension of P Systems, called P Systems with Membrane Channels (PMC Systems), in which membranes are enriched with channels and objects can pass through a membrane only if there are channels on the membrane that enable such a passage. We show that PMC Systems are universal even if only the simplest form of evolution rules is considered, and we give two application examples.
6
Content available remote Security in a Model for Long-running Transactions
Gruska D.P., Maggiolo-Schettini A., Milazzo P.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
189-203
EN
Communicating Hierarchical Transaction-based Timed Automata have been introduced to model systems performing long-running transactions. Here, for these automata a security concept is introduced, which is based on a notion of opacity and on the assumption that an attacker can not only observe public system activities, but also cause abortion of some of them. Different intruder capabilities as well as different kinds of opacity are defined and the resulting security properties are investigated. Security of long-running transactions is defined by the mentioned notion of opacity and conditions for compositionality are established.
7
Content available remote A P Systems Flat Form Preserving Step-by-step Behaviour
Barbuti R., Maggiolo-Schettini A., Milazzo P., Tini S.
Fundamenta Informaticae
|
2008
|
Vol. 87, nr 1
1-34
EN
Starting from a compositional operational semantics of transition P Systems we have previously defined, we face the problem of developing an axiomatization that is sound and complete with respect to some behavioural equivalence. To achieve this goal, we propose to transform the systems into a normal form with an equivalent semantics. As a first step, we introduce axioms which allow the transformation of membrane structures into flat membranes. We leave as future work the further step that leads to the wanted normal form.
8
Content available remote A Calculus of Looping Sequences for Modelling Microbiological Systems
Barbuti R., Maggiolo-Schettini A., Milazzo P., Troina A.
Fundamenta Informaticae
|
2006
|
Vol. 72, nr 1-3
21-35
EN
The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent elements and operators of sequencing, looping, containment and parallel composition. The looping operator allows tying up the ends of a sequence, thus creating a circular sequence which can represent a membrane. We show that a membrane calculus recently proposed can be encoded into CLS. We use our calculus to model interactions among bacteria and bacteriophage viruses, and to reason on their properties.
9
Content available remote A Probabilistic Model for Molecular Systems
Barbuti R., Cataudella S., Maggiolo-Schettini A., Milazzo P., Troina A.
Fundamenta Informaticae
|
2005
|
Vol. 67, nr 1-3
13--27
EN
We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a probabilistic transition system can be derived from it. We use the algorithm in the development of an interpreter for the model, which we use to simulate the evolution of molecular systems. In particular, we show the results of the simulation of a real example of enzymatic activity. Moreover, we apply the probabilistic model checker PRISM to the transition system derived by the model of this example, and we show the results of model checking of some illustrative properties.
10
Content available remote Compositional Synthesis of Generalized Mealy Machines
Tini S., Maggiolo-Schettini A.
Fundamenta Informaticae
|
2004
|
Vol. 60, nr 1-4
367--382
EN
We give an algorithm for synthesizing Generalized Mealy Machines from LTL-formulae. The main novelty of the paper is that the algorithm is compositional. Its complexity coincides with the lower bound of the synthesis problem.
11
Content available remote Dynamic Hierarchical Machines
Lanotte R., Maggiolo-Schettini A., Peron A., Tini S.
Fundamenta Informaticae
|
2003
|
Vol. 54, nr 2,3
237-252
EN
We present Dynamic Hierarchical Machines (DHMs), an extension of Communicating Hierarchical Automata allowing dynamic activation of components. We give an operational semantics of DHMs and we provide examples of modeling in the context of security. We characterize a fragment of DHMs which are equivalent to Recursive Hierarchical Machines and therefore to Pushdown Machines.
12
Content available remote Transformations of Timed Cooperating Automata
Lanotte R., Maggiolo-Schettini A., Tini S., Peron A.
Fundamenta Informaticae
|
2001
|
Vol. 47, nr 3,4
271-282
EN
The paper pursues the investigation of Timed Cooperating Automata (TCAs) by studying transformations which are suggested as means for stepwise TCA construction.
13
Content available remote Process algebras for network communication
Gruska D.P., Maggiolo-Schettini A.
Fundamenta Informaticae
|
2001
|
Vol. 45, nr 4
359-378
EN
Critical issues that arise when process algebras are used for protocol specifications are discussed. To overcome some of these problems, a process algebra for protocol specifications is presented. It is based on Milner's Calculus of Communicating Systems, which is enriched by time and network reasoning. Several bisimulation based semantics for the calculus are defined and their properties are discussed.
14
Content available remote Timed Cooperating Automata
Lanotte R., Maggiolo-Schettini A.
Fundamenta Informaticae
|
2000
|
Vol. 43, Nr 1-4
153-173
EN
We propose Timed Cooperating Automata (TC As), an extension of the model Cooperating Automata of Harel and Drusinsky, and we investigate some basic properties. In particular we consider variants of TCAs based on the presence or absence of internal activity, urgency and reactivity, and we compare the expressiveness of these variants with that of the classical model of Timed Automata (TAs) and its extensions with periodic clock constraints and with silent moves. We consider also closure and decidability properties of TCAs and start a study on succinctness of their variants with respect to that of TAs.
15
Content available remote Applying techniques of asynchronous concurrency to synchronous languages
Maggiolo-Schettini A., Tini S.
Fundamenta Informaticae
|
1999
|
Vol. 40, Nr 2,3
221-250
EN
In synchronous programming, programs can be perceived as purely sequential, and parallelism is only a logical concept useful to develop programs in a modular way. Classical semantics for synchronous languages interpret programs as sequential input/output finite state machines (i/o FSMs) where concurrency disappears. We argue that semantics where concurrency is reflected can be useful at least for improving hardware implementation, verification, and design of model-based schedulers. So, these semantics should not ``compete'' with the classical ones but should offer different, although consistent, views of programs, each supporting a particular task in their development. In order to define semantics reflecting concurrency, well established techniques adopted to define ``truly concurrent'' semantics for asynchronous languages could be applied. In this paper, we consider as a prototype of the class of synchronous languages the language Esterel, which is gaining use in a wide variety of applications. Then, following a method proposed by Degano and Priami to give semantics for asynchronous process algebras, we develop a semantic framework in which one can define different, although consistent, semantics of Esterel programs. The idea is to define a very concrete model of the language from which more abstract models can be recovered by means of suitable abstraction functions. We define a proved transition system (PTS) as the most concrete model of Esterel. We show that the classical interpretation in FSMs can be recovered from the PTS by a suitable abstraction function, namely we show that our most concrete semantics is consistent with the classical one. Then, from proved trees obtained by unfolding parts of the PTS, we abstract locality trees and enabling trees. We show how locality trees can be used to improve the hardware implementation of the language, namely to remove redundant latches generated by the compiler. Finally, we show how enabling trees can be used to improve the verification phase, namely to isolate program parts which actually cause the violation of a certain property.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.