Massimo Bartoletti

Giu 102014
 
Upcoming Seminar

Flow Unfolding of Multi-clock Nets

June 18, 14.30 (Lab 5)
Palazzo delle Scienze - Cagliari

Giovanni Casu
Dipartimento di Matematica e Informatica - University of Cagliari


Abstract.
Unfoldings of nets are often related to event structures: each execution of a net can be viewed as a configuration in the associated event structure. This allows for a clear characterization of dependencies and the conflicts betweenoccurrences of transitions in the net. This relation is somehow lost if more compact representations of the executions of nets are considered, e.g. in trellises or merged processes of multi-clock nets. This talk aims to expose the work "Flow Unfolding of Multi-clock Nets" which will be presented in the Petri Nets 2014 conference.

In this talk we introduce an unfolding, called flow unfolding, that turns out to be related to flow event structures, hence dependencies and conflict are still represented. Furthermore, this unfolding gives also a more compact representation of the executions of a multi-clock net, similarly to what approaches like trellises or merged processes do.
Mag 162014
 
Upcoming Seminar

Coinduction Up-To for Non Deterministic Automata

May 21, 11.00 (Aula F)
Palazzo delle Scienze - Cagliari

Filippo Bonchi
Ecole Normale Supérieure de Lyon - France


Abstract.
In this talk, I will introduce the Coinduction proof principle and its enhancements by mean of up-to techniques.
I will introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Such technique can be effectively implemented in an algorithm that exponentially improves the state of the art.
Giu 192013
 
Upcoming PhD course

Reversible Computing

July 15-19, 2013
Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Ivan Lanese
Università di Bologna & INRIA FOCUS Team

Abstract. Reversible computing emerges spontaneously in many areas, such as  quantum computing or biological modeling. Also, reversible computing
allows for recoverability: when an error occurs reversibility allows one to go back to a past state and try again. Reversibility is well  understood in a sequential setting: to reverse a computation one has  to recursively undo the last step. This is not possible in a concurrent scenario, since it may not be clear which the last performed action is.

We will study reversibility for concurrent interacting systems. In particular, we consider causal consistent reversibility, where only actions which have produced no consequences can be undone. We consider uncontrolled forms of reversibility first. However, uncontrolled  reversibility is not suitable for programming safe applications, since  backward steps should be triggered only when an error state is reached. To this end we define a rollback operator allowing the  programmer to control when backward steps are performed. We also show that specifying alternatives is useful to avoid looping behaviors. We  make our intuitions formal using reversible process calculi.  Finally, we discuss applications of our theory to transactions and to debugging.


The official presentation of the course will be on July 15 (Monday) in Aula C, at 10:00. The schedule of the course will be fixed during this meeting.

Course schedule.
  • Monday 15, 10.00-12.00 Aula F [slides]
  • Tuesday 16, 10.00-12.00 Aula F [slides]
  • Wednesday 17, 10.00-12.00 Aula C [slides]
  • Thursday 18, 10.00-12.00 Aula C [slides]
  • Friday 19, 10.00-12.00 Aula C [slides]

The course has been funded by the PhD Course in Computer Science of the University of Cagliari.

 Scritto da in 19 Giugno 2013  Events  Commenti disabilitati su PhD course: Reversible Computing
Giu 192013
 
Upcoming Seminar

A Tool for Verifying Bisimilarity in CCP

June 26, 10.00 (Aula F)
Palazzo delle Scienze - Cagliari

Andres Aristizabal
Pontificia Universidad Javeriana Cali - Colombia


Abstract.
Concurrent constraint programming (ccp) is a well-established formalism for specifying processes posting and querying (partial) information in shared-memory concurrent systems. Bisimilarity is recognized as the finest behavioural equivalence in concurrency theory.

In this talk we present a tool for verifying the adequate notion of bisimilarity in ccp [FoSSaCS'11] following the theoretical algorithms presented in [SAC'12] and [ICE'12]. Also we intend to describe the structure of the tool, thus, the steps which have to be followed in order to obtain an efficient and consistent tool.

All in all, we give the main insights of a web-based tool to verify strong and weak bisimilarity in ccp, i.e., preliminary concepts, the syntax used by the tool, some flowcharts describing important implemented algorithms, the structure of the tool and the way it works while interacting with an user.  

 Scritto da in 19 Giugno 2013  Events  Commenti disabilitati su Seminar: A Tool for Verifying Bisimilarity in CCP
Apr 152013
 
Upcoming Seminar

Lending Petri Nets (and contracts)

April 16, 15.00 (Aula F)
April 17, 11.00 (Lab. 5)
Palazzo delle Scienze - Cagliari

G. Michele Pinna
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari


Abstract.
In the first part of this seminar, we give a brief introduction to Petri nets, one of the classical models of distributed systems. Petri nets have been applied in various areas, among which the description and analysis of business processes.

In the second part, w
e present Lending Petri nets, a variant of Petri nets which allows places to "lend" tokens under the guarantee that credits will be honoured - that is, lent tokens are eventually returned.

Lending Petri nets are then exploited to model contracts for business processes. In particular, we show how they can be used to formalise contracts which protect themselves while still realizing the desired choreography. We relate Lending Petri nets with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.

Mar 012013
 
Upcoming Seminar

A Calculus of Controlled Monotonicity

March 5, 15.00
Aula F - Palazzo delle Scienze - Cagliari

Gabriele Pulcini
Dipartimento di Informatica - Scienza e Ingegneria - Università di Bologna


Abstract.
We introduce a cut-free logical system involving serio-parallel structures relying on preorders. This system describes processes displaying a
kind of controlled monotonicity (e.g. biochemical processes) by means of a specific variant of standard Gentzen-style sequents called "embedded sequents".

Gen 292013
 
The Trustworthy Computational Societies research group (TCS) of the University of Cagliari  is looking for two post-docs to join our ongoing projects.

We seek applicants with strong interest in some of the following topics: programming language design and implementation, concurrency theory, program analysis and verification, and security foundations. The successful candidates will in work in the TCS group at the Department of Mathematics and Computer Science, University of Cagliari (Italy).


The scientific core of the group is the development of formal methods for security of concurrent and distributed systems, and the experimentation of these methods through actual implementations. The team is composed by both researchers in the fields of security and concurrency theory (process algebras, semantics and types for concurrency, linear logic) and developers. A detailed presentation of the research group TCS can be found at the website tcs.unica.it.

Positions: 2 positions, each of 2 years and renewable for another year

Gross salary: ~23K EU / year

Requisites: applicants must hold a PhD in Computer Science, Mathematics or related discipline, and must produce evidence of expertise on the above-mentioned topics. The PhD degree must have been obtained not later than 10 years before the postdoc starts.

Starting date: may 2013 (with possibility of delaying until sept. on candidate request)

Location: Cagliari is located on the southern coast of Sardinia, the second largest island in the Mediterranean see. The Cagliari airport is only 15’ from the city centre, and it is connected with >70 direct flights (many of which are low-cost Ryanair flights) to Italy and Europe. The climate is Mediterranean, with mild winters (average temp. 16.4C) and many sunny days (~300 days/year without precipitation). The main beach, Poetto, is only 10’ from the city centre. The Department of Mathematics and Computer Science is hosted in the Palazzo delle Scienze, located on top of a hill nearby the historical area of Castello.

Inquires may be made to Massimo Bartoletti,
bart@unica.it.

Set 052012
 
Upcoming Seminar

Circularity, event structures, and contracts

Sept 11, 12.00
Aula C - Palazzo delle Scienze - Cagliari

Tiziana Cimoli
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari


Abstract.
Contracts will play an increasingly important role in the specification and implementation of distributed (cloud) systems. Quoting from [1], “Absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance”. Contracts describe the promised behavior of a software agent, from the point of view of the actions it may perform, the interactions it may participate into, and its goals. A primary use of contracts if that of postponing actual interaction with other agents until an agreement on the mutually promised behaviour has been found. As in the real world, promises are not always kept by software systems, and so contracts may be helpful also after the agreement to disciplinate the interaction among agents, and to establish liability in case of violations.

At a very abstract level, a contract can be seen as sets of events, together with relations to specify the causal dependencies and the conflicts between events. This seems to suggest event structures - one of the fundamental causal models for concurrency - as a natural candidate for representing contracts. For instance, one can interpret the enabling b|-a of a stable event structure as the contract clause “I will do a after you have done b”.

However, event structures do not capture a crucial aspect of contracts, i.e. the capability of reaching an agreement in the presence of circularity in the declared promises. For instance, one would expect that the contract where A promises a in change of b, and B promises b in change of a, has an agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only one configuration - the empty set. This is because a|-b actually models the fact that b may only happen after a has been done, and b|-a as the fact that a may happen after b - and so neither a nor b can happen. Of course, A could simply declare to do a, without asking b to be performed first - but this would not protect A from a misbehaving B.

To reconcile causality with circularity, A could relax her contract, i.e. she could do a in change of the promise of B to do b. In this case A can safely do the first step, because either B does b, or he will be culpable of a contract violation.

In this talk we present an extension of event structures which allows for this kind of reasoning. The contract a||-b (intuitively, “I will do a if you promise to do b”) reaches an agreement with the dual contract b||-a, while protecting the participant who offers it. We characterise configurations of these event structures as provability of formulae in the contract logic PCL, an extension of intuitionistic logic with a “contractual implication” connective.

We then focus on the problem of determining, in any state of the execution of a contract, which events have to be done next. This problem is trivial in classical event structures (one has to do the events whose causes have already been done), while it becomes relevant in the presence of circularity: indeed, before performing an event a (whose causes have not already been done) one has to be sure that its causes will be done, eventually in the future. Also in this case we devise a logical characterisation via an encoding in the logic PCL.

References

[1]  Michael Armbrust, Armando Fox, Rean Griffith, Anthony D. Joseph, Randy Katz, Andy Konwinski, Gunho Lee, David Patterson, Ariel Rabkin, Ion Stoica, Matei Zaharia. A View of Cloud Computing. Communications of the ACM, Vol. 53 No. 4, Pages 50-58, 2010
Lug 092012
 
Upcoming PhD course

Bisimulation, process algebras, and coinduction

July 2012
Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Emilio Tuosto
Department of Computer Science
University of Leicester (UK)

Abstract. After a brief (non technical) introduction of the abstract concept of bisimulation, the course will show how this notion can be used to define observational semantics of concurrent computations expressed as process algebras (with names). Finally, the course will highlight the coinductive nature of bisimulation and how to use coinduction to reason about the behaviour of concurrent (or diverging) applications.

The official presentation of the course will be on July 10 (Tuesday) in Aula Magna Matematica, at 18:00. The schedule of the course will be fixed during this meeting.

Course schedule.
  • Tuesday 10, 18.00-19.00 Aula Magna Matematica
  • Thursday 12, 18.00-19.00 Aula C
  • Monday 16, 15.00-17.00 Aula C
  • Tuesday 17, 15.00-17.00 Aula C

The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.


Lug 092012
 
Upcoming Seminar

Formal Models in Systems Biology

July 10,
16.00-18.00 Aula Magna Matematica,
July 12, 16.00-18.00 Aula C,
Palazzo delle Scienze - Cagliari

Andrea Bracciali
SICSA Lecturer - University of Stirling (UK)

Abstract. Papers like "Protein molecules as computational elements in living cells" [Bray, Nature 1995] and "Cells as computation" [Regev and Shapiro, Nature 2002] have put forward the idea that many aspects of living systems have a computational nature. Specifically, the complex network of interaction and information exchange that occurs within the biochemistry at the inter and intra cellular level, can be assimilated to the functioning of a distributed, interactive computational system. In the words of Bray, proteins are "functionally linked ... into biochemical 'circuits' that perform a variety of simple computational tasks including amplification, integration and information storage".

Under this perspective, it has appeared natural to employ the techniques used to model and analyse interactive computational systems to the realm of living organisms. Such a research trend aims at further developments within Systems Biology, the research area that approaches the study of the living organisms at a systemic level (see "Systems Biology: a brief overview" [Kitano, Science 2002]). Computationally inspired formal models and analysis techniques are being used to carry out "in silico" experiments, which may often represent a cheaper, faster, more ethical, more easily measurable, and less constrained complement to the more traditional "in vitro/vivo" investigation.

This extended-seminar will briefly survey some of the formal techniques, particularly those originated from concurrency theory, which have been adopted, adapted and further developed for the research in Systems Biology. Starting from a historical perspective, the main ideas of the approach will be discussed and a few small examples discussed.


The course has been funded by the Autonomous Region of Sardinia through the Visiting Professor Program 2011-12.


credits unica.it | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929
note legali | privacy

Nascondi la toolbar