• !! >>>> SYSTEM BIOLOGY: "A survey on formal methods in System Biology" (.pdf), from a talk by Linda Brodo - University of Sassari"




• !! >>>> IMPORTANT: about software patents in Europe.


• !! >>>> DIDATTICA [TEACHING (Programming Languages), in Italian]: "Laboratorio di Introduzione alla Programmazione"



• " Computer Science is embarrassed by the computer."

Research interests

Formal methods

Coordination

Security protocol analysis

Intelligent agents

Temporal reasoning

Short resume and brief research overview

Andrea Bracciali started his research activity during his Ph.D. studies, and has been carrying it out for several years. Driven by research curiosity, he has always had a quite large area of interest and has collaborated with a number of scientists, both young colleagues and affirmed senior researchers. After the period of training to research, during which he participated in several schools, his research record currently consists of more than twenty published works, co-authored with about twenty researchers from various European institutions. He has actively sought research collaborations with different researchers in his area, participating in research visits, with the University of Malaga and with the Imperial College, London, and distributed working groups (SOCS project: Univ.Pisa, Univ. Bologna, ICSTM London, City Univ. London, Cyprus Univ.), keeping a good record of contacts for present and future collaborations. He has been and is active in reviewing (conference proceedings and journals) and organisational activities (conference and local events organisation). He has taught university classes of core courses for the degree in Computer Science, as well as classes for professionals and professional training for private and public institutions, and has supervised Master thesis.

The main research topics of his Ph.D. studies have regarded specification languages and models for software compositions, with particular reference to the description of the behaviour of distributed components interacting in open environments. This research line is founded on formal methods (mainly based on process algebras) for the description of the behaviour of software components, their interaction and properties of component-based systems, with a particular interest when systems are ``open", i.e., informally speaking, they may not be completely specified or controllable and can evolve dynamically. In this context, the following points have been investigated:

• models for open and dynamic systems, e.g. in the context of WAN-computing, mobile code, Global Computing [2,3,23,6,12,17,18,19],
• the development of techniques for the correct composition of software components independently developed (component adaptation), e.g. within the Component-based Software Engineering context [3,14,15,16,21,23],
• the use of symbolic models for the design and verification of open software systems, and the development, starting from these models, of tools supporting (semi-)automated verification [6,12,20,24].

The above mentioned scenarios can not neglect the issues of security and the same approaches used to describe the interaction of autonomous components in open environment have been extended to address the verification of security protocols, seen as interaction amongst independent components in partially accessible, not fully specified, possibly malicious environment [22,23,13]. The use of abstract and symbolic techniques has also been exploited to make verification computationally more tractable, paving the way for combining the theoretical aspects with the practical implementation of verification tools, and discussing the more suitable methodological approaches [20].

A parallel research interest, sharing several characteristics with the ones above, is the field of (Multi) Agent Systems, intended as autonomous, possibly ``rational", components, interacting with each other. In particular, declarative approaches based on computational logic for the specification and verification of Multi-agent systems, abstract models for the behaviour of logic-deductive agents operating within open environments, and corresponding computational models (in particular, based on abductive logic) have been investigated [5,4,7,8,11]. Also in this case, the theoretical investigation has been contrasted with (prototypal) system development, like a software platform supporting agent reasoning and interacting within an open system. [1,10]

A specific offspring of the above research field is the more specific interest in reasoning about time and changes, i.e. reasoning about "actions and changes" and time flux within an open environment, that, other than the standard issues about time representation, e.g. persistency, also requires that consistency aspects of the representation used are dealt with. The developed theories have also been studied with respect to the computational models that may support them [9].

As far as concerns future research, my aim is to further investigate models and analysis techniques used to address the open issue of the (re-)definition of the overall cycle-life of applications operating within open systems, given that this metaphor is rapidly emerging as the most relevant computational model of the information society, and beyond. Indeed, emerging technologies are providing new globally distributed computing environments, which in turn are broadening and fostering the development of new kinds of pervasive applications in such a way that they are going to affect many aspects of our life. (e.g., broadly speaking, computational entities in our homes, cars, phones, hospitals, entertainment systems, administrative and financial offices tend to be integrated together in a seamless open system supporting, for instance, e-business, where individuals and even applications can establish economic transactions; e-health, with support for an overall assisted personal care; e-governance, with the possibility to extend democratic processes; and e-entertainment, like interactive tv-channels).

Moreover, the last years have shown surprising connections between life processes, like the cell chemistry, and computation, and these seem to be stronger when computation is intended as interaction of autonomous entities within open systems. The possible cross-fertilisations amongst the two fields are attracting a huge number of researchers, and the (hopefully mutual) application to life science of some of the research I carried out so far seems to me to be of strong interest and potentially much inspirational.

Finally, I am currently seeking a competitive and supporting working environment where I may enhance my research career and, also, contribute to the successful development of the hosting institution.

My coauthors

DISCLAIMER: As a contributing author of the documents listed in this page, I have made available our work electronically to ensure timely dissemination of scientific and technical contributions on a non-commercial basis. Nevertheless, copyright and all rights therein are maintained by the authors or by other copyright holders (e.g., the publisher). It is understood that all persons accessing this information will adhere to the appropriate copyright rules. In particular, these works may not be reposted without the explicit permission of the copyright holder.

Journals

A. Sorathiya, P. Liò and A. Bracciali ``Formal reasoning on qualitative models of coinfection of HIV and Tuberculosis and HAART therapy''. BMC Bioinformatics. 11(1): Asia Pacific Bioinformatics Conference. 2010.

A. Bracciali, M. Brunelli, E. Cataldo and P. Degano, ``Synapses as Stochastic Concurrent Systems''. Theoretical Computer Science. Elsevier. 408(1), pages 66-82, 2008. ( DOI: 10.1016/j.tcs.2008.07.008 ).

A. Bracciali, M. Brunelli, E. Cataldo and P. Degano, ``Stochastic models for the in silico simulation of synaptic processes''. BMC Bioinformatics. 9(4):S7 2008. [open access]

C. Bodei, A. Bracciali, D. Chiarugi, ``On Deducing Causality in Metabolic Networks''. BMC Bioinformatics. 9(4):S8 2008. [open access]

P. Baldan, A. Bracciali and R. Bruni, ``A Semantic Framework for Open Processes''. Theoretical Computer Science. Elsevier. 389(3), pages 446-483, 2007 ( DOI: 10.1016/j.tcs.2007.09.004 )  [related TR.pdf.tgz]

A. Bracciali, G. Ferrari and E. Tuosto, "A symbolic framework for multi-faceted security protocol analysis". International Journal of Information Security. Springer. Vol 7(1), 2008. (ISSN: 1615-5262, DOI 10.1007/s102070-007-0043-9). [.pdf]

A. Bracciali, U. Endriss, N. Demetriou, T. Kakas, W. Lu and K. Stathis, "Crafting the Mind of PROSOCS Agents". In Petta P., Müller J.P. (ed.): Best of "From Agent Theory to Agent Implementation 4", Applied Artificial Intelligence. Taylor and Francis. Vol 20(4-5), pages 105-131, 2006. [.pdf]

A. Bracciali, A. Brogi and F. Turini, "A framework for specifying and verifying the behaviour of open systems". The Journal of Logic and Algebraic Programming. Special Issue on Process Algebra and System Architecture. Elsevier. Vol 63(2), pages 215-240, 2005. [.pdf]

A. Bracciali, A. Brogi, and C. Canal, "A Formal Approach to Component Adaptation". Elsevier Journal of Systems and Software. Special Issue on Automated Component-Based Software Engineering. Elsevier. Vol 74(1), pages 45-54, 2005. [.pdf]

Book chapters

P. Degano and A. Bracciali, ``Process calculi, Systems Biology and Artificial Chemistry''. In G. Rozenberg, T.H.W. B\"{a}ck, and J.N. Kok editors Handbook of Natural Computing. Springer. 2010. To appear. (ISBN: 978-3-540-92911-6).

A. Bracciali, M. Brunelli, E. Cataldo and P. Degano, ``Formal models of the calyx of Held ''. In A. Condon, D. Harel, J.N. Kok, A. Salomaa, and E.Winfree editors Algorithmic Bioprocesses. Natural Computing Series. Springer. Pages 331-366, 2009. (ISBN: 978-3-540-88868-0 (Print) 978-3-540-88869-7 (Online) ).

Electronic journals

C. Bodei, A. Bracciali, and D. Chiarugi, "Control Flow Analysis for Brane Calculi". In Proc. of 2nd International Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2008), Elect. Notes in Theoret. Comp. Science vol. 227, Elsevier Science, 2009. (ISSN 1571-0661).

A. Bracciali, R. Bruni and A. Lafuente, "On symbolic semantics for name-decorated contexts". In Proc. of First Interaction and Concurrency Experience (ICE08 - ICALP2008 Workshop), Elect. Notes in Theoret. Comp. Science vol. 229, Issue 3, Elsevier Science, 2009. (ISSN 1571-0661). doi:10.1016/j.entcs.2009.06.038

A. Bracciali, G. Baldi, G. Ferrari, and E. Tuosto, "A Coordination-based Methodology for Security Protocol Verification". In Proc. of 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP04), Elect. Notes in Theoret. Comp. Science vol. 121, Elsevier Science, 2005. (ISSN 1571-0661). [.pdf]

A. Bracciali, A. Brogi, and C. Canal, "Systematic Component Adaptation". In A. Brogi, E. Pimentel, editors, Proc. FMCI, Formal Methods and Component Interaction (ICALP 2002 Satellite Workshop), Elect. Notes in Theoret. Comp. Science vol. 66(4), Elsevier Science, 2002. (ISBN 0444512799). [.pdf]

A. Bracciali, A. Brogi, G. Ferrari and E. Tuosto, "Security Issues in Component-based Design". In U. Montanari, V. Sassone, editors, Proc. ConCoord, International Workshop on Concurrency and Coordination, Elect. Notes in Theoret. Comp. Science vol. 54, Elsevier Science, 2001. (ISBN 0444510680). [.pdf]

Conferences and Workshops

G. Maggenti, A. Bracciali and P. Mancarella, ``Abduction and Legal Reasoning.'' In First International Conference on Forensic Applications and Techniques in Telecommunications, Information and Multimedia (e- Forensics'08), pages 1-6. Adelaide, Australia, 2008. ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering). (ISBN 978-963-9799-19-6).

A. Bracciali, M. Brunelli, E. Cataldo and P. Degano, ``Expressive Models for Synaptic Plasticity''. In Computational Methods in System Biology (CMSB'07), pages 152-167. Edinburgh, United Kingdom, 2007. Lecture Notes in Computer Science/LNBI 4695. Springer. (ISBN 978-3-540-75139-7). draft [.pdf]

A. Bracciali, M. Brunelli, E. Cataldo and P. Degano, ``In Silico Stochastic Simulation of Ca-triggered Synaptic Release''. In Nettab 2007. Pisa, Italy, 2007. [.pdf]

C. Bodei, A. Bracciali and D. Chiarugi ``A Toolkit Supporting Formal Reasoning about Causality in Metabolic Networks''. In Nettab 2007. Pisa, Italy, 2007. [.pdf]

P. Baldan, A. Bracciali, L.Brodo and R. Bruni, "Deducing Interactions in Partially Unspecified Biological Systems". In H. Anai, K. Horimoto and T. Kutsia editors. The 2nd International Conference on Algebraic Biology (AB'07), pages 262-276. Austria 2007, Lecture Notes in Computer Science 4545, Springer. (ISBN 978-3-540-73432-1). draft[.pdf]

A. Bracciali, P. Mancarella, K. Stathis, and F. Toni, "Stable Multi-agent systems". In M.P. Gleizes, A. Omicini and F. Zambonelli editors, Proc. of the 5th International Workshop on Engineering Societies in the Agents World (ESAW 2004), pages 322-334. Toulouse, France, 2004. Lecture Notes in Artificial Intelligence 3451, Springer. (ISBN 3-540-27330-1). [.pdf]

A. Bracciali, N. Demetriou, U. Endriss, A. Kakas, W. Lu, P. Mancarella, F. Sadri, K. Stathis, G. Terreni and F. Toni, "The KGP Model of Agency for Global Computing: Computational Model and Prototype Implementation". In P. Quaglia and C. Priami editors, Post-Proc. of the Global Computing 2004 Workshop, pages 342-369. Rovereto, Italy, 2004. Lecture Notes in Computer Science 3267, Springer. (ISBN 3-540-24101-9). [.pdf]

P. Baldan, A. Bracciali, and R. Bruni, "Symbolic Equivalences for Open Systems". In P. Quaglia and C. Priami editors, Post-Proc. of the Global Computing 2004 Workshop, pages 1-17. Rovereto, Italy, 2004. Lecture Notes in Computer Science 3267, Springer. (ISBN 3-540-24101-9). [.pdf]

A. Bracciali, P. Mancarella, K. Stathis, and F. Toni, "On Modeling Multi-agent Systems Declaratively". In Proc. of Declarative Agent Languages and Technologies (DALT 2004), pages 53-68. New York, NY, 2004. Lecture Notes in Artificial Intelligence 3476, Springer. (ISBN: 3-540-26172-9). [.pdf]

A. Bracciali and P. Torroni, "A new framework for knowledge revision of abductive agents through their interaction". In J. Dix and J. Leite editors, Proc. of Computational Logic in Multi-Agent Systems, Fourth International Workshop(CLIMA-IV), Revised Selected and Invited Papers, pages 159--177. Fort Lauderdale, FL, 2004. Lecture Notes in Artificial Intelligence 3259, Springer. (ISBN 3-540-24010-1). [.pdf]

A. Bracciali, and A. Kakas, "Frame Consistency: Computing with Causal Explanations". In J. Delgrande and T. Schaub editors, Proc of the 10th International Workshop on "Non-Monotonic Reasoning" (NMR2004), pages 79-87. Whistler BC, Canada, 2004. (ISBN 92-990021-0-X). [.pdf]

K. Stathis, A. Kakas, W. Lu, N. Demetriou, U. Endriss and A. Bracciali, "PROSOCS: a platform for programming software agents in computational logic". In R.Trappl editor Proc. of the 17th European Meeting on Cybernetics and Systems (AT2AI-4 -- EMCSR'2004) Austrian Society for Cybernetic Studies, Volume 2, pages 523-528. Austria, 2004. (ISBN 3-85206-169-5). [.pdf]

A. Bracciali and P. Torroni, "A new framework for knowledge revision of abductive agents through their interaction (preliminary report)". In J. Dix, J. Leite editors, Pre-Proc. of Computational Logic in Multi-Agent Systems (CLIMA-IV), pages 143-161. Fort Lauderdale, FL, 2004. (ISBN 3-89720-688-9). [.pdf]

P. Baldan, A. Bracciali and R. Bruni, "Bisimulation by Unification". In H. Kirchner, C. Ringeissen editors, Proc. 9th International Conference on Algebraic Methodology And Software Technology (AMAST'2002), pages 254-270. Reunion Island, 2002. Lecture Notes in Computer Science 2422, Springer. (ISBN 3-540-44144-1). [.pdf]

A. Bracciali, A. Brogi, G. Ferrari and E. Tuosto, "Security and Dynamic Compositions of Open Systems". In H.R. Arabnia editor, Proc. of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA02), pages 1372-1377, vol III. Las Vegas, NV, 2002, CSREA Press. (ISBN 1-892512-89-0). [.pdf]

A. Bracciali, A. Brogi and C. Canal, "Systematic Component Adaptation". In Proc. of IDEAS 2002 Workshop Iberoamericano de Engenharia de Requisitos e Ambientes Software, pages 340-351. La Habana, Cuba, 2002.

A. Bracciali, A. Brogi and C. Canal, "Adapting Components with Mismatching Behaviours". In J. Bishop editor, Proc. Component Deployment, First International IFIP/ACM Working Conference (CD02), pages 185-199. Berlin, Germany, 2002, Lecture Notes in Computer Science 2370, Springer. (ISBN 3-540-43847-5). [.pdf]

A. Bracciali, A. Brogi and C. Canal "Dynamically Adapting the Behaviour of Software Components". In F. Arbab, C. Talcott editors, Proc. 5th International Conference on Coordination Models and Languages (Coordination'02), pages 88-95. York, UK, 2002, Lecture Notes in Computer Science 2315, Springer. (ISBN 3-540-43410-0). [.pdf]

A. Bracciali, A. Brogi and F. Turini, "Interaction Patterns for Open Systems". In F.T. Rojas, J.E.A. Monge, Y.S. Sánchez editors, IDEAS 2001 Workshop Iberoamericano de Engenharia de Requisitos e Ambientes de Software, pages 398-407. San José, Costa Rica, 2001. [.pdf]

A. Bracciali, A. Brogi and F. Turini, "Coordinating Interaction Patterns" In Proceedings of the ACM Symposium on Applied Computing, pages 159-165. Las Vegas, NV. ACM, 2001. (ISBN 1-58113-287-5). [.pdf]

T. Bolognesi and A. Bracciali, "Formal specification of discrete systems by active predicates and dynamic constraints". In P. Ciancarini, A. Fantechi, R. Gorrieri, editors, Formal Methods for Open Object-based Distributed Systems, Proceedings of FMOODS'99, pages 161-168. Firenze, Italy. Kluwer Accademic Publishers, 1999. (ISBN 0-7923-8429-6).

Ph.D. Thesis

A. Bracciali, Behavioural Patterns and Software Composition, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, TD-03/03, 2003. [asbtract] [.ps.gz]

Other works

E. Cataldo, A. Bracciali, M. Brunelli and P. Degano, "Stochastic and executable models of synaptic processes". Frontiers in Neuroinformatics. Conference Abstract: Neuroinformatics 2008. doi: 10.3389/conf.neuro.11.2008.01.012

P. Mancarella, F. Toni and A. Bracciali (eds.) "Deliv- erable D8: A computational approach to (societies of) computees", 2004. Project "Societies of computees (SOCS)." The European Commission IST-2001-32530.

A. Bracciali, D.A. Baxter, M. Brunelli, E. Cataldo and P. Degano, "Ca2+ triggered vesicle release mechanisms: in silico experiments". The 37th annual meeting of the Society for Neuroscience, Nov. 3-7 San Diego, California. Society for Neuroscience, 2007. Online. [.pdf]

P. Baldan, A. Bracciali and R. Bruni, "A Semantic Framework for Open Processes", Technical Report, TR-07-09, Dipartimento di Informatica, Università di Pisa, 2007. [.ps.gz]

P. Baldan, A. Bracciali and R. Bruni, "Symbolic Equivalences for Open Systems", Technical Report, TR-03-16, Dipartimento di Informatica, Università di Pisa, 2003. [.ps.gz]

A. Bracciali, A. Brogi and F. Turini, "Interaction Patterns for Component Based Software Development" In CBD-TOOLS Component Based Development: Software Architecture, Component Models and Teaching. Workshop TOOLS-2000.

A. Bracciali, "Un'architettura metalogica per un sistema multiagente". Master Thesis, Dipartimento di Informatica, Università di Pisa. Giugno 1997.

2009     

European Molecular Biology Organization (EMBO). Short term fellowship.

2009

HPC-Europa2 Transnational Access Programme. Fellowship.

2009     

British-Italian Partnership Programme 2008-2009: ``Refining spatial information in computational models for systems biology'' [principal investigator].

2009

MIUR (PRIN07): ``SOFT: Security oriented formal techniques''

2007-2008

MIUR: ``Bisca: Bio-Inspired Systems and Calculi with Applications.''

2006

MIUR (Italian Ministry of Education, University and Research): ``Sybilla: Description and analysis of the behaviour of bio-cells.''

2002-2005

The European Commission IST-2001-32530: ``Societes of computees (SOCS)''

2002-2003

MIUR (Italian Ministry of Research and Education): ``NAPOLI: Network Aware Programming -- Objects, Languages, Implementations.''

1999-2000

Azione integrata Italia-Spagna: ``Linguaggi e modelli per l'interazione di componenti software (Languages and Models for the Interaction of Software Components).''

1998-2000

MURST (Italian Ministry of the University, and the Scientific and Technological Research): ``AI*IA: Agenti Intelligenti: Interazione e Acquisizione di conoscenza'' (Intelligent Agents: Interaction and Knowledge Acquisition).

Temporal reasoning

A Temporal Reasoner, based on the Abductive Event Calculus, has been developed within the SOCS project . Currently, two versions have been implemented by me and prof. Tony Kakas . The first one runs over the Kakas-Mancarella ALP proof procedure (implemented by Kakas and Ray), the second one runs over the CIFF proof procedure (implemented by Endriss), an extension of the Fung-Kowalski IFF proof procedure, developed within the same project. Both the implementations are supported by the Sicstus prolog engine.

If interested, please contact me.