PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 8

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 A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
Castiglioni V., Lanotte R., Tini S.
Fundamenta Informaticae
|
2016
|
Vol. 143, nr 1/2
51--71
EN
We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions occurring in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of formulas allowing linear and polynomial terms.
2
Content available remote A Specification Format for Rooted Branching Bisimulation
Castiglioni V., Lanotte R., Tini S.
Fundamenta Informaticae
|
2014
|
Vol. 135, nr 4
355--369
EN
Rule formats are sets of syntactical constraints over SOS rules ensuring semantical properties of the derived LTS. Given a rule format, our proposal is to relax the constraints imposed on each single rule and to introduce some constraints on the form of the whole set of rules, thus obtaining a new format ensuring the same semantical property and being less demanding than the original one. We apply our idea to a well known rule format for rooted branching bisimulation equivalence.
3
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.
4
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.
5
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.
6
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.
7
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.
8
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ć.