Nano-devices are molecular machines synthesized from molecular subcomponents whose functions are combined in order to perform the func- tion of the machine. It frequently results of relative motions of subcomponents triggered by chemical events such as excitement induced by light, acidity or tem- perature changes. Thus the function consists in the transformation of a chemical event into a mechanical event. An important and characteristic feature of these devices is their intrinsic compositional nature. Therefore process-algebra for- malisms are natural candidates for their modeling. To this aim we introduce a dialect of the -calculus, the nano calculus. It is a rule-based language, the basic agents are molecules, with explicit representa- tion of molecular complexations and internal states. Its stochastic semantics is governed by rules which correspond to chemical reactions. The stochastic rate of the rule, possibly in nite, corresponds to the kinetic rate of the reaction. We illustrated its relevance for the modeling and simulation of nano-devices with an example stemming from the collaboration with the chemistry department of bologna: the [2]RaH rotaxane. We modeled it in nano and simulated its behaviour under various conditions of concentration: rst we validate our model by checking its correspondance with the experimental data and then we investi- gate extreme conditions not observable in practice. We were able to show that some classical assumption about kinetic rates were not correct any longer in this setting. The calculus has many advantages for the modelling of biochemical sys- tems. It is in particular compact, easily reusable and modi able and maybe more importantly much biological-like and thus easier to learn for biochemists. On the other hand the -calculus, also often used to model biochemical sys- tems, has a much more developed theory and more available tools. We present an encoding from the nano calculus to the stochastic -calculus. It satis es a very strong correctness property: S ! T , [[S]] ! [[T]], where S and T are nano terms, is the rate of the reaction and [[:]] is the encoding. Thus it permits to use nano as a front-end formalism and still get the bene ts of the theory and tools of the -calculus. We carry on with a study of the chemical master equation. It probabilisti- cally describes the possible behaviours of the system over time as a di erential equation on the probability to be in a given state at a given instant. It is a key notion in chemistry. There have been many e orts to solve it, and methods such as the Gillespie's algorithm has been developed to simulate its solution. We introduce and motivate a notion of equivalence based on the chemical master equation. It equates state with similar stochastic behavior. Then we prove that this equivalence corresponds exactly to the notion backward stochastic bisimu- lation. This bisimulation di ers from the usual ones because it considers ingoing transitions instead of outgoing transitions. This results is worth in itself since it establishes a bridge between a chemical semantics and a computer semantics, but it is also the rst step towards a metrics for biochemistry. Finally we present an unexpected consequence of our study of the nano calculus. We study the relative expressiveness of the synchronous and asyn- chronous -calculus. In the classical setting the latter is known to be strictly less expressive than the former. We prove that the separation also holds in the stochastic setting. We then extend the result to the -calculi with in nite rates. We also show that under a small restriction the asynchronous -calculus with in nite rates can encode the synchronous -calculus without in nite rates. In- terestingly the separation results are proved using the encodability of the nano calculus. We also propose and motivate a stochastic -calculus with rates of di erent orders of magnitude: the multi-scale -calculus to which we generalize our results. Finally we prove that in the probabilistic settings the asynchronous -calculus can be encoded into the asynchronous one.

<p>Three issues will be elaborated and disussed in the proposed thesis. The first is<br />administration and control of data access rights in networks with XML data, with<br />emphasis on data security. The second is the administration and control of<br />access rights to data in computer networks with RDF data, with emphasis on<br />data privacy. The third is prevention of errors and memory leaks, as well as<br />communication errors, generated by programs written in Sing # language in the<br />presence of exceptions. For all three issues, there will be presented formal<br />models with corresponding type systems and showed the absence of undesired<br />behavior i.e. errors in networks or programs.</p> / <p>У тези су разматрана три проблема. Први је администрација и контрола<br />права приступа података у рачунарској мрежи са XML подацима, са<br />нагласком на безбедости посматраних података. Други је администрација и<br />котрола права приступа подацима у рачунарској мрежи са RDF подацима,<br />са нагласком на приватности посматраних података. Трећи је превенција<br />грешака и цурења меморије, као и грешака у комуникацији генерисаним<br />програмима написаних на језику Sing# у којима су присутни изузеци. За сва<br />три проблема биће предложени формални модели и одговарајући типски<br />системи помоћу којих се показује одсуство неповољних понашања тј.<br />грешака у мрежама односно програмима.</p> / <p>U tezi su razmatrana tri problema. Prvi je administracija i kontrola<br />prava pristupa podataka u računarskoj mreži sa XML podacima, sa<br />naglaskom na bezbedosti posmatranih podataka. Drugi je administracija i<br />kotrola prava pristupa podacima u računarskoj mreži sa RDF podacima,<br />sa naglaskom na privatnosti posmatranih podataka. Treći je prevencija<br />grešaka i curenja memorije, kao i grešaka u komunikaciji generisanim<br />programima napisanih na jeziku Sing# u kojima su prisutni izuzeci. Za sva<br />tri problema biće predloženi formalni modeli i odgovarajući tipski<br />sistemi pomoću kojih se pokazuje odsustvo nepovoljnih ponašanja tj.<br />grešaka u mrežama odnosno programima.</p>