Testo italiano

Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi.

Testo inglese

Theory of Concurrency, Higher Order and Types

MONTANARI	UGO
(cognome)	(nome)
Università degli Studi di PISA	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

ugo@di.unipi.it
(E-mail)

HONSELL	FURIO
(cognome)	(nome)

Professore ordinario	20/08/1958	HNSFRU58M20D969M
(qualifica)	(data di nascita)	(codice di identificazione personale)

Università degli Studi di UDINE	Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI
(università)	(facoltà)
K05B	Dipartimento di MATEMATICA E INFORMATICA
(settore scient.discipl.)	(Dipartimento/Istituto)

0432/558467	0432/558499	honsell@dimi.uniud.it
(prefisso e telefono)	(numero fax)	(E-mail)

K05B

Testo italiano
LOGICAL FRAMEWORKS ; TEORIA DEI TIPI ; SINTASSI ASTRATTA DI ORDINE SUPERIORE ; METODI COALGEBRICI ; LAMBDA CALCOLO ; PROGRAMMAZIONE CONCORRENTE CON VINCOLI ; LINGUAGGI DI COORDINAMENTO ; SICUREZZA ; AUTOMI PER SISTEMI IN TEMPO REALE

Testo inglese
LOGICAL FRAMEWORKS ; TYPE THEORY ; HIGHER ORDER ABSTRACT SYNTAX ; COALGEBRAIC METHODS ; LAMBDA CALCULUS ; CONCURRENT CONSTRAINED PROGRAMMING ; COORDINATION LANGUAGES ; SECURITY ; REAL-TIME AUTOMATA

Testo italiano

Laurea in Matematica presso l'Universita` di Pisa (1981), Diploma in Matematica presso la Scuola Normale Superiore di Pisa (1983). Professore ordinario (K05B) presso l'Universita` di Udine dal 1990. Ha ricoperto posti di ricerca e/o di ruolo presso il Dipartimento di Informatica dell'Universita` di Torino (Ricercatore 1993-1995), Edinburgh University (Research Fellow in Computer Science 1996-1998), Universita` di Udine (professore associato K05B 1989-1990). Responsabile di unita` nei progetti della CE: HCM Lambda Calcul Type', EC SCIENCE MASK, ESPRIT WG TYPES. Membro di comitato di programma e ``invited speaker'' per varie conferenze internazionali. Membro dell' ``editorial board'' della rivista internazionale MSCS. Membo permanente dell' IFIP WG 2.2. Interessi di ricerca: semantica dei linguaggi di programmazione, lambda calcolo, logiche dei programmi, teorie dei tipi, logical frameworks, metodi logici, topologici e categoriali in informatica. contributi di ricerca: teoria degli insiemi non ben fondati, modelli e teorie del lambda calcolo, logical frameworks, lambda calcoli di oggetti.

Testo inglese

Laurea in Mathematics (1981, Pisa University), Diploma In Matematica (1983,Scuola Normale Superiore, Pisa). Full professor in Computer Science at Udine University since 1990. Research and academic positions previously held at Torino University (Ricercatore in Computer Science 1983-1985), Edinburgh University (Research Fellow in Computer Science 1986-1988), Udine University (Associate Professor in Computer Science 1989-1990). Site Leader of EC HCM Lambda Calcul Type', EC SCIENCE MASK, ESPRIT WG TYPES. PC member and invited speaker to international conferences. Member of the the editorial board of MSCS. Member of the IFIP WG 2.2. Research interests: semantics of programming languages, program logics, lambda-calculus, type theory, logical frameworks, logical topological and categorical methods in informatics. Research contributions: non-wellfounded set theory, models and theories of lambda calculus, logical frameworks, lambda calculi of objects.

1. HONSELL F., HONSELL F., PLOTKIN G., "A Framework for Defining Logics" , Rivista: Journal of ACM , Volume: 40(1) , pp.: 143-184 , (1993) .
2. FISHER K., HONSELL F., MITCHELL J., "A Lambda Calculus of Objects and Method Specialization" , Rivista: Nordic Journal of Computing , Volume: 1(1) , pp.: 3-37 , (1994) .
3. HONSELL F., MICULAN M., SCAGNETTO I., "pi-calculus in (Co)Inductive Type Theory" , Rivista: Theoretical Computer Science , pp.: 42 , (1998) in corso di pubblicazione .
4. HONSELL F., LENISA M., MONTANARI U., PISTORE U., "Final Semantics for the pi-calculus" , Rivista: PROCOMET'98,Chapman & Hall , pp.: 225-243 , (1998) .
5. DI GIANANTONIO P., HONSELL F., LIQUORI L., "A Lambda Calculus of Objects with Self-inflicted Extension" , Rivista: ACM-SIGPLAN OOPSLA-98 , Volume: 333(10) , pp.: 166--178 , (1998) .

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
						1999	2000
1	HONSELL	FURIO	MATEMATICA E INFORMATICA	Prof. ordinario	K05B	11	8
2	ALESSI	FABIO	MATEMATICA E INFORMATICA	Ricercatore	K05B	11	8
3	GABBRIELLI	MAURIZIO	MATEMATICA E INFORMATICA	Prof. associato	K05B	11	6
4	MAZZANTI	STEFANO	MATEMATICA E INFORMATICA	Ricercatore	K05B	8	6
5	PERON	ADRIANO	MATEMATICA E INFORMATICA	Ricercatore	K05B	11	8

1.10.2 Personale universitario di altre Università

Nº	Cognome	Nome	Università	Dipart./Istituto	Qualifica	Settore scient.	Mesi uomo
							1999	2000

1.10.3 Titolari di assegni di ricerca

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo

1.10.4 Titolari di borse per Dottorati di Ricerca e ex L. 398/89 art.4 (post-dottorato e specializzazione)

Nº	Cognome	Nome	Dipart./Istituto	Anno del titolo	Mesi uomo
1.	CIAFFAGLIONE	ALBERTO	MATEMATICA E INFORMATICA	1998	12
2.	FRANCO	GIANLUCA	MATEMATICA E INFORMATICA	1995	8
3.	LIQUORI	LUIGI	MATEMATICA E INFORMATICA	1996	5
4.	SCAGNETTO	IVAN	MATEMATICA E INFORMATICA	1997	14

1.10.5 Personale a contratto da destinare a questo specifico programma

Nº	Qualifica	Costo previsto	Mesi uomo
1.	Dottorato in Informatica	30	11

1.10.6 Personale extrauniversitario dipendente da altri Enti

Nº	Cognome	Nome	Dipart./Istituto	Qualifica	Mesi uomo
1.	LENISA	MARINA	LFCS-Edinburgh	Research fellow	6
2.	MICULAN	MARINO	INFN-Trieste	Tecnologo	6

Testo italiano

Teoria e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla Teoria dei Tipi, per assistere nell'utilizzo di metodi formali. Sviluppo e studio di metodi formali di specifica, analisi e verifica, basati sulla semantica, per calcoli di oggetti, linguaggi di coordinamento e sistemi in tempo reale.

Testo inglese

Theory and experiment of interactive proof development environments, for assisting in the use of formal methods, based on Type Theoretical Logical Frameworks. Investigation of formal methods, based on semantics, for object calculi, coordination languages and real time systems.

Testo italiano

Teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi

Molte ricerche ed esperimenti sono stati condotti, dalla fine degli anni 80, su ambienti interattivi computerizzati, per assistere nelle derivazioni formali, basati sulla teoria dei tipi (e.g. [HHP,COQ],TYPES WG). La teoria dei tipi offre molti vantaggi come Logical Framework, ovvero come linguaggio di specifica per sistemi formali. In primo luogo permette di utilizzare la Sintassi Astratta di Ordine Superiore (HOAS) nella specifica della sintassi e della semantica operazionale dei linguaggi oggetto. Questo fa si che molti operatori di legame su variabili e nomi possano essere espressi in modo uniforme e algebrico. L'HOAS risulta quindi molto utile sia come metaformalismo per esprimere caratteristiche sintattiche dipendenti dal contesto, sia come standard per quanto concerne il trattamento dell'alfa conversione e dello ``scope''. Ma i Logical Frameworks permettono/costringono anche l'utente a formulare il proprio sistema in Deduzione Naturale (NDS) cosi`da rendere esplicita la dipendenza tra assunzioni e conclusioni, ovvero la relazione di conseguenza logica utilizzata. Sia l'HOAS che l'NDS pertanto suggeriscono la possibilita` di riformulare i sistemi oggetto in modo piu` astratto, meno legato ai dettagli di una particolare presentazione e piu` appropriato per il ragionamento formale assistito dal computer. Queste riformulazioni, ancorche' utilissime, sono pero` abbastanza problematiche per quanto concerne alcuni sistemi. Ricadono tra questi i formalismi per ragionare su processi (di ordine superiore) quali [MPW,AG,Bou]. A causa della natura complessa dei loro operatori di legame questi sistemi beneficerebbero notevolmente di un'analisi in termini di HOAS o dall'esistenza di ambienti interattivi per essi. Fino ad oggi pero` tali sistemi non sono stati studiati in questo senso. Il gruppo di Udine ha una notevole esperienza nel campo della specifica di sistemi formali in Logical Frameworks [HM,AHMP,HLMP,MMS]. Uno degli aspetti piu` problematici riguardanti l'uso di sistemi in HOAS concerne il fatto che anche nei Logical Frameworks piu` potenti, quali [COQ], non e` possibile sviluppare adeguatamente la metateoria dei sistemi oggetto. Una possibile via d'uscita assiomatica a questo problema e` stata proposta dai ricercatori di questo gruppo in [HMS]. Recentemente Hofmann [Hof] ha mostrato come sia possibile usare modelli di prefasci per dimostrare la consistenza di alcuni assiomi di [HMS]. Anche Plotkin [MPS] e Pitts [GP] hanno recentemente utilizzato idee basate su categorie di funtori per la trattazione matematica della sintassi astratta di linguaggi con operatori di legame. Lo studio delle correlazioni tra l'approcio assiomatico di [HMS] e quello categoriale sembra molto promettente.

Lambda calcoli di oggetti

Sin dalla pubblicazione del lavoro di Fisher,Honsell e Mitchell [FHM], i lambda calcoli di oggetti, ovvero i lambda calcoli con primitive per manipolare oggetti, hanno suscitato molto interesse, si veda ad esempio [AC]. L'utilita` di rappresentare in lambda calcolo una nozione risiede nel fatto che cio` permette di avere una comprensione concettuale migliore della nozione in questione ed una sua trattazione operazionale piu` astratta. Il lambda calcolo di oggetti in [FHM] formalizza un linguaggio ad oggetti ``delegation-based'' che contiene sia il lambda calcolo che primitive per creare, modificare e aggiornare oggetti. In [FHM] e` stato inoltre proposto un sistema di tipi che permette di prevenire staticamente errori del tipo ``messaggio non compreso''. Un gran numero di estensioni e varianti di tale calcolo sono state proposte in letteratura per trattare ad esempio sottotipi e oggetti incompleti, [BBDL,Liq]. C'e` ancora molta strada da percorrere pero` prima di poter disporre di una teoria quadro per i lambda calcoli di oggetti.

Analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini

Recentemente i metodi coinduttivi e coalgebrici per la specifica della semantica operazionale dei linguiaggi di programmazione hanno riscosso notevole successo e interesse [BMMR,Rut]. Questi metodi forniscono infatti principi, elementari ma potenti, per ragionare sul comportamento infinito di programmi, processi ed altri tipi di dati di ordine superiore. Specialmente quando vengono usati in combinazione con tecniche basate su relazioni logiche, essi permettono una trattazione strutturata degli oggetti infiniti attraverso le loro rappresentazion sintattiche, mantenendo cosi` limitata la sovrastruttura matematica necessaria. Honsell e Lenisa da molti anni studiano la Semantica Finale, un particolare approccio categoriale alla coinduzione, specialmente in categorie di insiemi [HL95,Len96,HLMP,Len98a,Len98b]. Molte sono ancora le questioni aperte in questo ambito pero`. Mazzanti [Ma95,Ma97] studia da anni il problema della caratterizzazione della semantica di costrutti iterativi su tipi di dati. La sua linea di indagine e` attualmente basata sugli operatori di chiusura. Honsell, Lenisa [HL98] e Alessi [ABBR] studiano da molti anni varie categorie di domini ordinati e metrici per la semantica dei linguaggi di programmazione. Vi sono ancora molti problemi aperti in questo ambito soprattutto per quanto concerne la completezza di tali categorie e la possibilita` di ottenere descrizioni coinduttive di equivalenze osservazionali. Un importante problema e` anche quello di come ``parzializzare'' domini metrici mediante domini effettivi ordinati.

Modelli semantici e metodologie di verifica per linguaggi di coordinamento

La programmazione concorrente con vincoli (ccp) [SRP] e' un paradigma di programmazione asincrono nel quale la memoria, diversamente all'interpretazione classica, e' vista come un ``vincolo''. Dato che i vincoli e le operazioni di sincronizzazione e comunicazione possono essere espressi in termini logici, e' possibile ottenere in modo relativamente semplice metodologie di verifica [BGMP] e di analisi [FGMP93]. Recentemente sono state studiate estensioni di ccp per applicazioni real-time (introducendo una nozione di clock ed opportuni costrutti) [SJG,BGM], per applicazioni distribuite (sostituendo la memoria globale con una collezione di memorie locali) ed infine per permettere la rimozione di informazione dalla memoria (usando nozioni basate su logica lineare). Tutte queste estensioni sono interessanti nel contesto dei linguaggi di coordinamento, sia come spunto per nuove proposte, sia perche' i relativi modelli semantici possono essere utilizzati per studiare alcuni dei linguaggi esistenti.

Automi per sistemi in tempo reale

Sono state proposte in anni recenti varie classi di automi adatti a modellare sistemi in tempo reale. Il confronto fra classi differenti di automi viene fatto tradizionalmente basandosi sul potere espressivo, su proprieta' di decidibilita', e piu' recentemente, sulla capacita' di esprimere descrizioni sintetiche. Inoltre, sono state tradizionalmente stabilite delle forti connessioni tra la teoria degli automi e le logiche per la specifica di sistemi in tempo reale. In questo contesto, siamo interessati alla logica degli automi sistolici ad albero binario introdotta in [MP] e usata in [MPP] per definire una teoria (decidibile) monadica del secondo ordine su strutture con un numero infinito di domini temporali lineari approssimabili. La teoria in questione consente di esprimere in modo naturale quelle proprieta' dei sistemi in tempo reale che fanno riferimento a scale temporali diverse.

Testo inglese

Theory, applications, and experiment of proof development environments based on type theoretic Logical Frameworks

Since the late '80's there has been extensive research and experiment in using proof development environments based on intuitionistic type theory for computer assisted formal reasoning (see e.g. [HHP,COQ], TYPES WG ). When taken as a Logical Framework, i.e. as a specification language for formal systems, type theory offers many advantages. First it allows for Higher Order Abstract Syntax (HOAS) to be used in the specification of the object syntax and its operational semantics; thereby allowing to express binding operators on variables, names, and locations in a uniform and algebraic way. HOAS is in fact extremely valuable both as a formalism for capturing certain context sensitive aspects of syntax, and for setting a standard on how scope and alpha conversion should be handled in formal systems. But Logical Frameworks allow/urge also the user to present his system in a natural deduction style (NDS), thereby making explicit the dependency between assumptions and conclusions, i.e. the consequence relations involved. Both HOAS and NDS suggest new presentations of the original logical systems which are much closer to the semantics, free form the irrelevant details of a specific presentation and more appropriate in mechanized formal reasoning. However, such reformualtions are often difficult to obtain. A case in point concerns (higher order) process and nominal calculi e.g. [MPW,AG,Bou]. Because of the complex nature of the operators on variables and names which they feature, these systems could greatly benefit from HOAS analyses and proof development environments generated by Logical Frameworks. However, up to now, very little has been carried out in this direction. The Udine group has a solid experience in tailoring formal systems for Type Theoretic Logical Frameworks (see e.g. [HM,AHMP,HLMP,MMS]).
A problematic theoretical issue concerning HOAS is the following: even in powerful Logical Frameworks such as COQ, metatheoretic reasoning on systems in HOAS is limited. In [HMS] the researchers in this proposal have outlined a viable axiomatic methodology to overcome these drawbacks. Recently M.Hofmann [Hof] has shown how suitable presheaf models can be used to prove consistency of some of those axioms. Also G.Plotkin et al.[FPT], and A.Pitts et al. [GP] have used recently ideas based on functor categories for structuring mathematically the syntax of systems involving binders. There seems to be a lot to be done in comparing the methodology of [HMS] with the functor theoretic approach.

Lambda calculi of Objects

Since the publication of [FHM] by Fisher, Honsell and Mitchell, there has been growing interest in calculi for objects, i.e. in lambda calculi extended with primitives for defining and manipulating objects, see e.g.[AC]. The ultimate goal in embedding new programming concepts in a lambda-calculus setting is to achieve a better conceptual understanding and a more abstract and general operational treatment of the concept under consideration. We can in fact capitalize on the extensive successful theoretical work that has been carried out in lambda calculus because of its principled and mathematically tractable syntax and semantics. The lambda calculus of objects of [FHM] formalizes a small delegation-based language which contains both lambda calculus and object primitives for creating, updating, and sending messages to objects. In [FHM] also a sound type assignment system is introduced, which allows to check statically if errors of the kind ``message not understood'' will not arise at run time. A number of extensions, or variants of the original language and type system, have been investigated by many researchers in this proposal, including Liquori [BBDL,Liq], and many typing disciplines which deal e.g. with subtypes and incomplete objects have been considered. Much remains to be done however in developing a general framework for lambda calculi of objects.

Categorical analysis of coinduction, algebraic analysis of
iteration and fine analysis of categories of domains

Recently, see e.g. [BMMR,Rut], there has been much interest on coalgebraic and coinducitve methods for the specification of operational semantics of programming languages. Such methods provide powerful proof principles for reasoning on the infinite behaviours of programs, processes, and objects of higher order data-types (e.g. exact reals). Especially when used in connection with techniques based on logical relations, they allow to reason on infinite objects in a mathematically principled and structured way, just by considering syntactical representations, thereby keeping the mathematical superstructure to a minimum. Honsell and Lenisa have been investigating Final Semantics, a particular categorical approach to coinduction, for quite some time [HL95,Len96,Len98a,Len98b,HLMP], especially in set theoretic categories based on hypersets. The whole area of operationally based semantics, however, appears to be full of yet unresolved general questions. S. Mazzanti [Ma95,Ma97] has been investigating for many years the old, but surprisingly not yet completely solved, problem of characterizing the semantics of iterative constructs on data types. His current line of approach is that of using closure operations on preorders. F.Honsell, M.Lenisa [HL98b] and F.Alessi [ABBR] have been investigating various metric and ordered categories of domains used in the semantics of programming languages, for many years. There are still many important open questions in this area especially with respect to the completeness of such categories and the possibility of providing coinductive characterizations of observational equalities. A problematic issue is also that of embedding metric spaces in effective domains.

Semantic models and verification methodologies for coordination
languages

Concurrent constraint programming (ccp) [SRP] is an asynchronous (concurrent) programming paradigm where the classical notion of store-as-valuation is replaced with the notion of store-as-constraint. Since constraints and the notions of communication and synchronization can be formalized in logical terms, one can obtain in a rather straightforward way a proof-theory [BGMP] and analysis tools [FGMP93] for ccp. Recently ccp has been extended for real-time applications (by introducing a notion of clock and suitable primitives) [SJG,BGM], for distributed computing (by replacing the global store with several local stores) and for allowing removal of information from the store (by using a linear logic setting). All these extensions are relevant in the context of coordination languages since they can inspire new proposals and their semantics models can be used to study existing languages.

Real time automata

Various classes of timed and synchronous automata have been proposed which are capable of modelling real time systems. Different classes of automata are usually compared with respect to their expressive power, the decidability of some basic properties and, more recently, "succinctness" of their representation of real time systems. Moreover, strong connections have been shown between automata and logical theories for the specification of real time systems. In particular, the logical theory of binary tree systolic automata, introduced in [MP], has been recently exploited in [MPP] for defining a decidable monadic second order theory over an infinite number of coarsable linear temporal domains. That theory allows to naturally express properties of real time systems which refer to times of different temporal granularity.

• [ABBR] Alessi, Baldan P. Bellè G. Rutten J.: Solutions of Functorial and Non-Functorial Metric Domain Equations, MFCS'95 Electronic Notes in Computer Science, Abstract available in Theoretical Computer Science 152, pp.321-332.
  
• [AC] M. Abadi, L. Cardelli: A Theory of Objects Springer Verlag, 1996.
  
• [AHMP98] Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano: Encoding Modal Logics in Logical Frameworks. Studia Logica, 60,(1), 1998.
  
• [AG] M. Abadi, A. Gordon: A Calculus for Cryptographic Protocols: The Spi Calculus.Information and Computation 148(1) pp. 1-70, 1999. Academic Press.
  
• [BGM] F.S. de Boer, M. Gabbrielli, and M.C. Meo. Semantics and expressive power of a timed concurrent constraint language. In G. Smolka. editor, Proc. Third Int'l Conf. on Principles and Practice of Constraint Programming (CP 97), Lecture Notes in Computer Science. Springer-Verlag, 1997.
  
• [BGMP] F.S. de Boer, M. Gabbrielli, E. Marchiori and C. Palamidessi: Proving Concurrent Constraint Programs Correct. Transactions on Programming Languages and Systems (TOPLAS), 19(5): 685-725, ACM Press, 1997.
  
• [BMRR] B.Jacobs et al. : Proc. 1st Wkshp. on coalgebraic methods in CS, ENTCS 11, 1998.
  
• [Bou] G.Boudol: The pi-calculus in direct style. Higher-Order and
  Symbolic Computation Vol 11, pp. 177-208, 1998
  
• [BBDL]V.Bono, M.Bugliesi, M.Dezani and L.Liquori: A Subtyping forExtendible, Incomplete Objects. Fundamenta Informaticae. to appear
  
• The COQ proof assistant reference manual - INRIA
  
• [DGHL] P.Di Gianantonio, F.Honsell, and L.Liquori: A Lambda Calculus of Objects with Self-Inflicted Extension In Proc. of ACM-SIGPLAN OOPSLA-98, Vol 33, Number 10, October 1998, pp 166--178, ACM Press.
  
• [DFP] R. De Nicola, G. Ferrari, R.Pugliese. Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering,
  24(5):315-330, IEEE Computer Society Press, 1998.
  
• [FGMP93] M. Falaschi, M. Gabbrielli, K. Marriott and C. Palamidessi: Compositional analysis of concurrent constraint languages. In Proc. Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 93), pages 210-221. IEEE Computer Society Press, 1993.
• [FGMP97] M. Falaschi, M. Gabbrielli, K.Marriott and C. Palamidessi: Confluence in Concurrent Constraint Programming. Theoretical Computer Science, 183, pp. 281-315, 1997.
• [FPT] M.Fiore, G.PLotkin, D.Turi: Abstract Syntax and Variable Binding, to appear in LICS'99.
  
• [Gel] D. Gelernter: Generative Communication in Linda. ACM TOPLAS 7(1), 1985.
  
• [GP] J.Gabbay, A.Pitts: A new approach to abstract syntax involving binders, to appear in LICS'99.
  
• [Hof] M.Hofmann: Semantical Analysis of higher order abstract syntax
  to appear in LICS'99
  
• [HHP] R. Harper, F. Honsell, G. Plotkin: A framework for Defining Logics.
  Journal of ACM,Vol. 40, No. 1, (1993), 143-184.
  
• [HL95] F. Honsell, M. Lenisa; Final semantics for untyped lambda calculus, TLCA'95, Springer LNCS 902, 1995.
  
• [HL98]F. Honsell, M. Lenisa: Semantical Analysis of Perpetual Strategies in lambda-calculus to appear in Theoretical Computer Science 213 , 1998.
  
• [HLMP] F. Honsell, M. Lenisa, U. Montanari, and M. Pistore Final Semantics for the pi-calculus, Programming Concepts and Methods PROCOMET'98, D. Gries et al. eds., Chapman & Hall, 1998.
  
• [HM] F.Honsell, M.Miculan: A natural Deduction approach to Dynamic Logic. Springer LNCS 1158, 1996.
  
• [MMS] F. Honsell, M. Miculan, I. Scagnetto: pi-calculus in (Co)Inductive Type Theory aparira` su Theoretical Computer Science.
  
• [Len96] M. Lenisa; Final semantics for a higher order concurrent language, CAAP'96, Springer LNCS 1059. 1996
  
• [Len98a] M.Lenisa: Themes in Final Semantics Ph.D. Thesis TD-6/98, March 1998. Dipartimento di Informatica, Università di Pisa.
  
• [Len98b] M.Lenisa: A Complete Coinductive Logical System for Bisimulation Equivalence of Circular Objects, to appear in ETAPS '99
  
• [Liq] L.Liquori : On Object Extension. In ECOOP-98, Springer LNCS 1445, pp 498 522, 1998.
  
• [LLL] F.Lang, P.Lescanne, L.Liquori: A Framework for Defining Object Calculi" ENS Lyon RR 1998-51, 1998.
  
• [Ma95] Mazzanti S.: Succint Iterative Characterizations of Primitive Computable Unary Functions, Information Processing Letters 56, pp. 315-319, 1995.
  
• [Ma97] S. Mazzanti: Iterative characterizations of computable unary functions: a general method, Mathematical Logic Quarterly 43 (1997) 29-38.
  
• [MP98] A. Monti and A. Peron: A Logical Characterization of Systolic Languages, Proceedings International Symposium on Theoretical Aspects of Computer Science (STACS'98), LNCS 1373, pp. 466--476, 1998.
  
• [MP9?] A. Monti and A. Peron: Systolic Tree omega-Languages: The Operational and the Logical View, Theoretical Computer Science, to appear.
  
• [MPP] A. Montanari, A. Peron and A. Policriti: Theories of omega-layered metric temporal structures: Expressiveness and Decidability, Logic Journal of the IGPL, 1999, to appear.
  
• [MPW] R.Milner, J.Parrow, D.Walker. A calculus of mobile processes. Inforamtion and Computation, 100(1):1-77, 1992.
  
• [Rut] J.J.M.M. Rutten: Universal coalgebra: a theory of systems, CWI CS-R9652,1996.
  
• [SJG] V.A. Saraswat, R. Jagadeesan, and V. Gupta: Foundations of
  Timed Concurrent Constraint Programming. In S. Abramsky editor, Proc. of the Ninth IEEE Symposium on Logic in Computer Science, pages 71--80. IEEE Computer Press, July 1994.
  
• [SRP] V.A. Saraswat, M. Rinard, and P.Panangaden: Semantic Foundation of Concurrent Constraint Crogramming. In Proc. Eighteenth ACM Symposium on Principles of Programming Languages, pages 333-353. ACM Press, 1991.

Testo italiano

Come e` stato fatto nella presentazione della base di partenza scientifica, distingueremo l'attivita` di ricerca dell'unita` di Udine in 5 filoni:

• teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi,
• lambda calcoli di oggetti,
• analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini,
• modelli semantici e metodologie di verifica per linguaggi di coordinamento,
• automi per sistemi in tempo reale.

Per ciascuno di questi filoni specificheremo a quale tematica del progetto nazionale e` correlato, discuteremo gli obiettivi generali e daremo il piano di lavoro specifico suddividendolo nei due anni.

Teoria, applicazioni e sperimentazione di ambienti interattivi generati da Logical Frameworks basati sulla teoria dei tipi (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto, A.Ciaffaglione) - Tematiche 7,2

I calcoli di processi (di ordine superiore), recentemente introdotti per la specifica e verifica di protocolli, come ad esempio lo spi calcolo [AG] e il blu calcolo [Bou], non sono stati fino ad oggi rappresentati in Logical Frameworks basati sulla teoria dei tipi, ne' analizzati dal punto di vista della HOAS. Sviluppando la metodologia che abbiamo introdotto in [HMS] per l'archetipo di tali calcoli, ovvero il pi-calcolo di Milner et al. [MPW], noi intendiamo codificare tali sistemi in HOAS, e sperimentare con gli ambienti interattivi generati da queste codifiche in COQ [COQ]. Sia gli utilizzatori che gli ideatori di tali sistemi dovrebbero beneficiare di queste analisi sintattiche astratte e delle implementazioni da esse generate. Tali calcoli hanno infatti sintassi piuttosto complesse e sono piuttosto difficili da manipolare senza sussidi automatizzati. Questi esperimenti dovrebbero condurre alla costruzione di un ``workbench'' assistito dal computer, basato su COQ, per l'analisi e la verifica della sicurezza nei protocolli di comunicazione. Questi esperimenti dovrebbero anche aiutarci pero` a delineare una metodologia generale per rappresentare e ragionare su ``nominal calculi'' e calcoli di processi in HOAS. Per poter sviluppare nei Logical Framework anche la metateoria di questi sistemi , dovremo pero` estendere la teoria dei tipi con nuovi assiomi e/o principi di induzione/ricorsiva e coinduzione. Solo cosi` si potranno infatti superare le limitazioni intrinseche delle teorie dei tipi nel trattare la metateoria di sistemi in HOAS. Questo approccio assiomatico, originariamente adoperato in [HMS] ci permette di mantenere trasparente la codifica e allo stesso tempo di contenere la complessita` della sovrastruttura matematica. Il nostro obiettivo ultimo, in questo ambito, e` quello di definire un sistema consistente di principi metalogici per ragionare su sistemi arbitrari in HOAS. Questo approccio pero` necessita di accurate analisi semantiche per dimostrare la consistenza del tutto. Recentemente Hofmann [Hof] ha mostrato come utilizzare categorie di funtori per modellare teorie dei tipi intuizionistiche e ha suggerito come tali modelli possano essere usati per dimostrare la consistenza degli assiomi di [HMS]. Intendiamo sviluppare nei dettagli queste dimostrazioni di consistenza e studiare la semantica delle teorie dei tipi nelle categorie di prefasci di Hofmann. Vorremmo anche confrontare il nostro approccio assiomatico all'analisi sintattica di linguaggi con operatori di legame, con quello categoriale di Plotkin [FPT] e con quello insiemistico di Pitts [GP]. Intendiamo sviluppare dei ``case studies'' di notevoli dimensioni in COQ, non solamente nella verifica di protocolli, e nella metateoria dei calcoli di processi di ordine superiore, ma anche nella computazione esatta sui reali. Quest'ultima sembra essere un'area che puo` beneficiare notevolmente dell'uso di assistenti computerizzati. Gli obiettivi specifici sono:
Primo anno: Intendiamo sviluppare numerose codifiche in HOAS di calcoli funzionali e di processi di ordine superiore quali lo spi calcolo, il blu calcolo ed il nu calcolo. Intendiamo svolgere ulteriori esempi di sviluppo in COQ della metateoria di sistemi in HOAS, quali FOL e il lambda calcolo. Cio` dovrebbe permetterci di perfezionare il sistema di assiomi per ragionare su contesti in HOAS di [HMS]. Intendiamo inoltre dimostrare la consistenza di tutti gli assiomi di [HMS] mediante modelli di prefasci.
Secondo anno: Intendiamo esplorare ulteriormente i modelli di prefasci per teorie dei tipi e dimostrare la consistenza di tutti gli assiomi della teoria generale dei contesti in HOAS. Intendiamo anche studiare una metodologia per dimostrare l'adeguatezza delle codifiche, basata su questi modelli. Intendiamo inoltre condurre ampi case studies in COQ di derivazione formale della metatoria dei calcoli di processi di ordine superiore e di loro applicazioni.

Lambda calcoli di oggetti (F.Honsell, L.Liquori) - Tematica 1

Vogliamo proseguire l'indagine sulle estensioni del lambda calcolo di oggetti di [FHM], lungo le linee di [DGHL]. In [DGHL] Di Gianantonio, Honsell e Liquori hanno introdotto un sistema di tipi piu` potente di quello originale che permette agli oggetti di estendere se stessi. Questo possibilita` sembra molto interessante anche per le sue possibili applicazioni ad altri linguaggi ad oggetti quali Java. Ma vi sono molte altre possibili estensioni del sistema di [FHM]. Oltre a rafforzare il sistema di tipi, si puo` estendere il linguaggio, garantendo a metodi e messaggi lo status di oggetti di prima classe. Si possono considerare sistemi di tipi espliciti, o un linguaggio con le sostituzioni esplicite invece del lambda calcolo. Si possono considerare inoltre varianti imperative di tutti questi calcoli. E` chiaro che non c'e` ancora ``il'' lambda calcolo di oggetti. E` nostra intenzione cercare di sviluppare una tale teoria quadro per calcoli di oggetti dove ambientare e studiare tutte le possibili varianti di [FHM]. A tal fine intendiamo trarre ispirazione da [DGHL] e dalla recente attivita` di Liquori all'ENS-Lyon [LLL]. In[LLL] viene presentato infatti un ``framework'' generale, Obj+a, per la semantica operazionale di linguaggi di oggetti con particolare attenzione agli aspetti funzionali e imperativi. Piu` specificamente il programma e`:
Primo anno: completare l'indagine teorica del sistema di tipi introdotto in [DGHL], e proseguimento dello sviluppo di Obj+a.
Secondo anno: definizione di un framework generale per i lambda calcoli di oggetti.

Analisi categoriale della coinduzione, analisi algebrica dell'iterazione e analisi della struttura fine di varie categorie di domini (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione) - Tematiche 3,5

Ci sono numerosi problemi aperti in queste aree. In primo luogo e` ancora da chiarire, eccetto che nel caso di alcuni semplici linguaggi, in che modo la semantica operazionale (finale) si correli alla semantica iniziale, e come e perche' sia possibile in alcuni casi, e non in altri, ottenere delle buone descrizioni coinduttive di semantiche operazionali interessanti. Anche lo stesso problema di come si rapportino i vari approcci categoriali alla coinduzione, ovvero coalgebre, ``span'' di morfismi aperti, fibrazioni, e` ancora irrisolto. Cosi` come lo e` quello di determinare quanto fedelmente ciascuno di questi approcci riesca a catturare la generalita` della coinduzione insiemistica. Intendiamo affrontare tutti questi problemi e studiare in particolare il potere espressivo e l'ambito di applicabilita`dell'approccio coalgebrico alla coinduzione e alle funzioni coiterative. Intendiamo studiare, al riguardo, come esprimere coalgebricamente vari principi di coinduzione generalizzati basati ad esempio su: bisimulazioni a meno, bisimulazioni non uniformi, bisimulazioni n-arie. Vogliamo studiare anche come estendere il paradigma coalgebrico ai funtori misti. Particolare attenzione verra` dedicata allo studio dell'ambito di applicabilita` di categorie insiemistiche concrete. L'interesse di cio` deriva dal fatto che in tali categorie la sovrastruttura matematica e` ridotta. Sempre nello spirito di studiare principi dimostrativi matematicamente elementari basati sulla sintassi, ma questa volta nella direzione delle relazioni logiche, intendiamo studiare una generalizzazione delle relazioni logiche capace di rendere conto del processo di ``data refinement'' nei linguaggi di ordine superiore. Gli operatori di chiusura su preordini saranno studiati sia dal punto di vista della teoria dei grafi sia da quello della teoria delle categorie, al fine di caratterizzare la semantica di costrutti iterativi per programmi non determinsitici e con comportamenti infiniti. Intendiamo inoltre continuare lo studio della struttura fine dei modelli di linguaggi di ordine superiore, quali il lambda calcolo, allo scopo di individuare nuovi principi di coinduzione. Verranno anche affrontati un certo numero di problemi specifici e diversificati relativi alla semantica matematica dei linguaggi di programmazione. Ad esempio verra` studiata la corrispondenza tra semantica metrica e semantica ordinata, e saranno studiati sistemi di tipo per catturare proprieta` computazionali. Il programma specifico e`:
Primo anno: Intendiamo sviluppare la teoria matematica delle relazioni prelogiche. Queste sono una generalizzazione delle relazioni logiche chiuse pero` per composizione. Intendiamo inoltre sviluppare altri esempi di descrizioni coalgebriche di principi di coinduzione insiemisitici. Useremo varie nozioni categoriali, quali quella di relatore, al fine di ottenere una certa generalita`. Intendiamo studiare operatori di chiusura su preordini dal punto di vista della teoria dei grafi per specificare la semantica di costrutti iterativi.
Secondo anno: Intendiamo continuare l'indagine del potere espressivo e dell'ambito di applicazione della Semantica Finale. Intendiamo sviluppare ulteriori esempi di caratterizzazioni coinduttive di equivalenza osservazionali, specialmente per quanto riguarda linguaggi e calcoli di ordine superiore che manipolano nomi. Intendiamo studiare gli operatori di chiusura dal punto di vista categoriale. Intendiamo infine studiare numerosi esempi su come ``parzializzare'' domini metrici al fine di individuare possibili criteri generali.

Modelli semantici e metodologie di verifica per linguaggi di coordinamento (M.Gabbrielli) - Tematica 6

Vari linguaggi di coordinamento esistenti sono basati sul paradigma ``Linda'', nel quale i processi comunicano mediante un unico ``spazio delle tuple''. Recentemente la formulazione originale di Linda [Gel85] e' stata estesa per trattare applicazioni distribuite ed per modellare la mobilita' di processi [DFP98]. Si studieranno quindi i nuovi aspetti semantici che sorgono nel contesto di tali estensioni, con particolare attenzione alle metodologie di verifica ed alle problematiche di sicurezza. Il programma specifico e`:
Primo anno: Si studieranno modelli semantici per alcuni linguaggi di coordinamento proposti recentemente e basati su estensioni del paradigma ``Linda''. Dato che tale paradigma ha varie caratteristiche in comune con la programmazione concorrente con vincoli (ccp), si cerchera' di adattare ad esso i modelli semantici (fully abstract) precedentemente sviluppati per estensioni temporizzate di ccp [BGM97]. Inoltre si studiera' il potere espressivo delle varie estensioni di Linda proposte, con particolare riguardo alle primitive aggiunte per descrivere mobilita' di processi. Infine si analizzera' la possibilita' di integrare programmazione concorrente con vincoli e linguaggi basati su Linda.
Secondo anno: Si studieranno metodologie di verifica per linguaggi di coordinamento basati su Linda che supportino la mobilita' di processi. In particolare si considereranno tecniche basate sulla logica temporale per affrontare problematiche di sicurezza.

Automi per sistemi in tempo reale (A.Peron) - Tematica 4

Si e' interessati ad individuare modelli di automi in grado di fornire descrizioni sintetiche di sistemi in tempo reale. Oggetto dello studio sara' l'influsso sulla complessita' della specifica dei diversi modi di esprimere il tempo e le condizioni temporali in varie classi di automi temporizzati (e.g. Timed automata, Timed Communicating automata etc.). Si intende introdurre anche una classe di automi capaci di reagire alla lettura di un simbolo con una sequenza possibilmente non unitaria di transizioni. (L'estensione trova ragione nella necessita' di rappresentare semplicemente led sequenze di transizioni istantanee dei sistemi reattivi sincroni.) Si vuole verificare se anche questa caratteristica influenza la complessita' della descrizione. Si vogliono studiare, inoltre, tecniche di ritemporizzazione. Per quanto concerne la relazione tra automi e logica, si intende introdurre il corrispettivo del frammento al primo ordine della logica degli infiniti domini approssimabili definita in [MPP99]. Ci si attende che questa logica modale sia una estensione (propria) della ben nota Propositional Linear Temporal Logic e sia anche la controparte logica della classe dei linguaggi accettati da automi sistolici ad albero e definibili al primo ordine. Inoltre, si affrontera' il problema di individuare una caratterizzazione logica di automi sincroni di potere espressivo maggiore a quelli considerati. Il programma specifico e`:
Primo anno: Si studiera' la complessita' della rappresentazione di varie classi di automi temporizzati e si fornira' la caratterizzazione modale del frammento al primo ordine della logica definita in [MPP99].
Secondo anno: Si introdurranno automi temporizzati con sequenze istantanee di transizioni e si studieranno, per questo modello, tecniche di raffinamento. Si studieranno caratterizzazioni logiche per altre classi di automi sincroni.

Testo inglese

As we did above, in illustrating the background to our research, we shall present the specific research activity proposed by the group in Udine by dividing it into 5 main areas, namely:

• theory, applications, and experiment of proof development environments based on type theoretic Logical Frameworks
  
• Lambda Calculi of objects
  
• categorical analysis of coinduction, algebraic analysis of
  iteration and fine analysis of categories of domains
  
• semantic models and verification methodologies for coordination languages
  
• real time automata.
  

For each of the above we will discuss the broad objectives of the proposed research, give a more detailed work plan, and indicate to which theme of the national project it belongs to.

Theory, applications, and experiments of proof development environment based on type theoretic Logical Frameworks (F.Honsell, F.Alessi, M.Miculan, I.Scagnetto, A.Ciaffaglione) - Thmes 7,2

Little experiment in type theoretic Logical Frameworks, has been carried out so far for (higher order) process calculi for protocol specification and verification. Building on our recent successful treatment in [HMS] of the archetype of such calculi, i.e. the pi-calculus of Milner et al [MPW], we intend to develop and experiment with HOAS implementations in COQ [COQ] of other such calculi e.g. the spi calculus [AM] and the blue calculus [Bou]. Due to the complex nature of the binding operators featured by these systems, both designers and users of such systems should benefit from our type theoretical accounts of the syntax and the operational semantics, and our implementations. Ultimately these experiments should lead to a comfortable computer assisted workbench, based on Coq, for protocol and security verification. These experiments should lead also to the design of a general methodology for representing and reasoning on nominal calculi and other higher order calculi in HOAS. In order to be able to carry out the necessary metatheoretic reasoning, however, it is likely that we will have to extend existing type theoretic metalanguages with new axioms and induction-recursion-coinduction principles. Type theory has, in fact, a limited power in supporting metatheoretic reasoning over systems in HOAS. Our approach, as pioneered in [HMS], is that of introducing suitable axiom packages. This allows us to maintain the transparency of the encoding and to keep the mathematical superstructure low. Our ultimate goal in this respect is to define a consistent and complete axiom system of metalogical principles for reasoning on arbitrary systems presented in HOAS. However so doing we will have to deal with the issue of consistency of the overall theory. Recently Hoffman [Hof] has showed how functor categories can be fruitfully put to use in modeling Intuitionistic Type Theories and hinted at how such models could be used to prove consistency of non-standard induction principles and axiom systems such as the ones we introduce. We intend therefore to develop full consistency proofs for our axioms systems using presheaf models in the style of Hofmann. We will compare also our axiomatic approach to reasoning on languages, with bindings and other operators on variables and names, to the categorical one of Plotkin [FPT] and the set-theoretical one of Pitts [GP]. Applications of the presheaf technique to proofs of adequacy will be explored also.
We expect to carry out some significant case studies using COQ not only on communication protocol verification, and the metatheory of higher order process calculi, but also on exact real number computation. This is an area which can benefit greatly from computer assistance in its formal developments.
The detailed work-plan is as follows:
First year: Develop more encodings in HOAS of functional calculi and, possibly higher order, process calculi such as the spi calculus, the blue calculus and the nu-calculus. Carry out more formal metatheoretic developments for such systems and other systems in HOAS such as FOL and lambda calculus. We hope thus to be able to finalize our metatheoretic axioms for reasoning on contexts over systems in HOAS. Prove formally the consistency of the axioms introduced in [HMS] using presheaf models.
Second year: We plan to explore further functor category models of type theory and prove the consistency of all our axioms for contexts in HOAS. We intend to investigate these models also for streamlining proofs of adequacy. Some large case studies on the metatheory and applications of higher order process calculi will be carried out.

Lambda calculi of Objects (F.Honsell, L.Liquori) - Theme 1

We want to carry on the investigation of significant extensions of the original lambda calculus of objects of [FHM] along the lines of [DGHL]. In [DGHL] Di Gianantonio, Honsell and Liquori introduced a strengthening of the original type system of that calculus which allows objects to extend themselves upon receiving a message. This is an interesting possibility, which has potential applications to practical object oriented languages sush as Java. But extensions of the original lambda calculus of objects can go in various other directions. Not only, one can strengthen the type system. One can also extend the language so as to allow methods and messages to be first class citizens; one can consider explicitly typed versions of the system, or replace the lambda calculus with a calculus of explicit substitutions. Furthermore one can introduce imperative versions of all these. It is apparent that there is no general lambda calculus of objects yet. One of the most important research problems in this area is to try to introduce and develop a framework language where to accomodate all these variants. It is our intention to try to develop such a general framework of objects, building both on [DGHL] and the current work that Liquori is doing at ENS-Lyon [LLL]. In [LLL] Liquori studies a general framework, Obj+a, for the foundation of operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues.
More specifically our work plan is as follows:
First year: complete the theoretical investigation of the type system introduced in [DGHL], and pursue the investigation of Obj+a.
Second year: design a general framework language for lambda calculi of objects.

Categorical analysis of coinduction, algebraic analysis of iteration and fine analysis of categories of domains (F.Honsell, M.Lenisa, S.Mazzanti, F.Alessi, A.Ciaffaglione) - Themes 3,5

There are many open problems in this area. First of all it is still unclear, apart form very simple languages, how operational (final) semantics exactly relates to initial semantics, and why and how can we get good coinductive characterizations of interesting semantical equivalences. Even the problem of how do the various categorical approaches to coinduction (e.g. coalgebras, span of open maps, fibrations) relate to one another and how much can they capture of the generality of set theoretic coinduction is still far form being settled. We intend to investigate such issues and in particular to study the expressive power and scope of the coalgebraic approach to coinduction and coiterative functions. In particular we intend to consider how to express various generalized coinduction principles based on e.g. bisimulation up-to principles, non uniform bisimulations, n-ary bisimulations. We intend to address also the problem of how to extend the coalgebraic paradigm to mixed functors. We shall also pursue our investigation of the scope of final semantics in elementary set-theoretic categories. Still in the spirit of syntactically based proof principles, but more in the line of logical relations, we intend also to develop a theory of generalized logical relations suitable for accounting the process of data refinement in higher order languages. Closure relations on preorders will be investigated both in the style of graph theory and in the style of category theory, to construct a semantics of iterative constructs for non terminating and non deterministic programming. We intend to continue the investigation of the fine structure of domain models of higher order programming languages such as lambda calculus, with the purpose of deriving new coinduction prniciples. A number of related specific semantical problems will be also addressed, e.g.: the correspondence between ordered and metric semantics, and the characterization of properties using type assignment systems. More specifically the work-plan in this area is the following:
First year: we intend to develop the mathematical theory of prelogical relations, a suitable genralization of logical relations, closed under composition. Develop more case studies in final semantics and in coagebraic descriptions of coinduction principles, using categorical notions, such as that of relator, for achieving generality. Study closure operators on preorders in the style of graph theory in order to construct a semantics of iterative constructs for non terminating and non deterministic programming.
Second year: We intend to continue the investigation of the scope and expressive power of Final Semantics. Develop more case studies in coinductive characterizations of operational equivalences, especially in connection with higher order languages and calculi, possibly involving names. Investigate closure operators categorically. Investigate general principles and more case studies in partializing metric domains.

Semantic models and verification methodologies for coordination languages (M.Gabbrielli) - Theme 6

Several existing coordination languages are based on the ``Linda'' paradigm, where processes communicate via a unique global ``tuple space'' on which a few primitive operations are defined. Recently the original formulation of Linda [Gel] has been extended to deal with distributed applications and to model mobility of processes [DFP]. We plan to investigate the new semantic and proof-theoretic issues which arise in the context of these extensions, with a particular attention to security related problems.
First year: we will study semantic models for some existing coordination languages based on extensions of the ``Linda'' paradigm. Since such a paradigm is similar to concurrent constraint programming (ccp), we plan to base our study on previous results we obtained for timed ccp [BGM97]. We will also investigate the expressive power of several existing extensions of Linda, and in particular we will consider the primitives which have been introduced for describing mobile agents. Finally we will consider possible integrations of ccp with Linda based coordination languages.
Second year: we will concentrate on verification methodologies for Linda based languages for mobile computing. In particular we will study techniques based on temporal logics for dealing with security issues.

Real time automata (A.Peron) - Theme 4

Our investigation will focus on various classes of timed and synchronous automata aimed at evaluating, under suitable criteria, their ability of describing real time systems. A criterion of evaluation will be "succinctness" of description. Harel and Drusinsky proved that (finite state) automata endowed with parallelism and communication features allow an exponential saving when compared with usual sequential finite state automata. In the same line, we shall consider whether different ways of representing time and different ways of expressing temporal constraints in varoius classes of automata (e.g. Timed automata, Timed Communicating automata etc.) affect the complexity of the specification. We want also to introduce automata able to read a symbol and to react by taking sequences of transitions (instead of one only transition, as usual). (This extension is motivated by the need of easily modeling instantaneous reactions in synchronous formalisms.) We want to investigate whether this new feature affects the complexity of the specification. For this extension we shall study retiming techniques. As far as the connection between automata and logic, we are also interested in investigating the logical counterpart of suitable classes of synchronous automata. We want to introduce the modal counterpart of the first order fragment of the logic of infinitely coarsable temporal domains in [MPP]. This modal counterpart is expected to be a (proper) extension of the well known Propositional Linear Temporal Logic as well as the (modal) logic counterpart of the class of first order definable languages accepted by systolic binary tree automata. Finally, we shall investigate the problem of defining a logic characterisation of other (more expressive) classes of synchronous automata.
First year: we shall study succinctness of different classes of timed automata and we shall provide the modal characterisation of the first order
fragment of the logic of infinitely coarsable temporal domains in [MPP99].
Second year: we shall introduce automata with instantaneous firing of sequences of transitions and we shall study, for this model, retiming techniques. We shall investigate the problem of defining a logic characterisation of other (more expressive) classes of synchronous automata.

Nº	Anno di acquisizione	Descrizione
		Testo italiano	Testo inglese
1.	1995	SUN - Sparc Station 20	SUN - Sparc Station 20
2.	1998	PC Scenic Celsius 2000 - Siemens	PC Scenic Celsius 2000 - Siemens
3.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX
4.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX
5.	1998	PC Pentium 200 MMX	PC Pentium 200 MMX

Attrezzatura I
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

Attrezzatura II
Descrizione

valore presunto (milioni)   percentuale di utilizzo per il programma

QUADRO RD

4.1.1 Altro

QUADRO RA

4.2.1 Altro

Firma ____________________________________________

(per la copia da depositare presso l'Ateneo e per l'assenso alla diffusione via Internet delle informazioni riguardanti i programmi finanziati; legge del 31.12.96 n° 675 sulla "Tutela dei dati personali")

Firma ____________________________________________	29/03/1999 16:51:32