Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca
INIZIO_TESTO_DA_INDICIZZARE

PROGRAMMA DI RICERCA 2005

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
Classificazione geografica
Bibliografia
(Missing references can be found in Models B.)
[AGO04]S.Abramsky,D.Ghica,L.Ong,A.Murawski.Applying Game Semantics to Compositional Software Modelling and Verification,TACAS'04
[AJM00]S.Abramsky,R.Jagadeesan,P.Malacaria.Full Abstraction for PCF.I&C 163
[BBB02]P.Baldan,A.Bracciali,R.Bruni.Bisimulation by unification.AMAST02
[BCE+99]P.Baldan,A.Corradini,H.Ehrig et al.Concurrent Semantics of Algebraic Graph Transformation Systems.
[BCEH04]P.Baldan,A.Corradini,H.Ehrig,R.Heckel.Compositional semantics for open Petri nets based on deterministic processes.MSCS15
[BCM01]P.Baldan,A.Corradini,U.Montanari.Contextual Petri nets,asymmetric event structures and processes.I&C,171
[BCM02]P.Baldan,A.Corradini,U.Montanari.Bisimulation equivalences for graph grammars.Formal and Natural Computing, LNCS2300
[BCM99]P.Baldan,A.Corradini,U.Montanari.Unfolding and Event Structure Semantics for Graph Grammars.FoSSaCS'99
[BCMR03]P.Baldan,A.Corradini,U.Montanari,L.Ribeiro.Coreflective concurrent semantics for single-pushout graph grammars.WADT'02
[BG01]R.Bruni and F.Gadducci.Some algebraic laws for spans.Relational Methods in Soft.,ENTCS 44.
[BGM02]R.Bruni,F.Gadducci and U.Montanari.Normal forms for algebras of connections.TCS 286
[BHLM04]R.Bruni,F.Honsell,M.Lenisa,M.Miculan.Modeling fresh names in the pi-calculus using abstractions.CMCS'04
[BMM02]R.Bruni,J.Meseguer and U.Montanari.Symmetric monoidal and cartesian double categories as a semantic framework for tile logic.MSCS 12
[BMM02a]R.Bruni,J.Meseguer and U.Montanari.Tiling transactions in rewriting logic.F.Gadducci and U.Montanari,ed.,WRLA'02
[BMR01]R.Bruni,U.Montanari and F.Rossi.An interactive semantics of logic programming.Theory and Practice of Logic Progr.6
[BMS05]R.Bruni,U.Montanari and V.Sassone.Observational congruences for dynamically reconfigurable tile systems.TCS.
[CC04]L.Cardelli and L.Caires.A Spatial Logic for Concurrency,II.TCS 322(2).
[CG00]L.Cardelli and A.Gordon.Mobile ambients.TCS 240
[CG02]A.Corradini and F.Gadducci.A functorial semantics for multi-algebras and partial algebras.TCS 286,p.293-322.
[CG99]A.Corradini and F.Gadducci.Rewriting on cyclic structures.Theoretical Informatics and Appl.33,p.467-493.
[CHM02]A.Corradini,R.Heckel and U.Montanari.Compositional SOS and beyond.TCS 280.
[CLW93]A.Carboni,S.Lack and R.F.C.Walters.Introduction to extensive and distributive categories.JPAA,84(2)
[CS96]G.Cattani and V.Sassone.Higher dimensional transition systems.LICS'96.
[CSW04]A.Cherubini,N.Sabadini and R.F.C.Walters.Timing in the Cospan-Span Model.COMETA 2004.
[CW87]A.Carboni and R.F.C.Walters.Cartesian bicategories.Pure and Applied Algebra 49
[Cai04]L.Caires.Behavioural and spatial observations in a logic for the pi-calculus
[Cor96]A.Corradini.Concurrent graph and term graph rewriting.CONCUR'96
[DMM96]P.Degano,J.Meseguer,U.Montanari.Axiomatizing the algebra of net computations and processes.Act.Inf.,33
[DP92]P.Degano and C.Priami.Proved trees.ICALP'92.
[EHPP04]H.Ehrig,A.Habel,J.Padberg,U.Prange.Adhesive high-level replacement categories and systems.ICGT'04
[FMT05]G.Ferrari,U.Montanari,E.Tuosto.Model checking for nominal calculi.FoSSaCS'05
[FPT99]M.Fiore,G.Plotkin,D.Turi.Abstract Syntax and Variable Binding.LICS'99
[FT01]M.Fiore,D.Turi.Semantics of name and value-passing.LICS'01
[Fio05]M.Fiore.Mathematical Models of Computational and Combinatorial Structures.FOSSACS'05
[GH97]F.Gadducci and R.Heckel.An inductive view of graph transformation.WADT'97.
[GH98]F.Gadducci and R.Heckel.An inductive view of graph transformation.LNCS 1376
[GHL99]F.Gadducci,R.Heckel, M.LlabrËs.A bi-categorical axiomatisation of concurrent graph rewriting.CTCS'99
[GL05]F.Gadducci and A.Lluch-Lafuente.Graphical verification of a spatial logic for the pi-calculus.Submitted.
[GM00]G.Gadducci and U.Montanari.The tile model.Proof,language and interaction.
[GM01]F.Gadducci and U.Montanari.A concurrent graph semantics for Mobile ambients.MFPS'01
[GMKSW01]F.Gadducci,U.Montanari,P.Katis,N.Sabadini and R.F.C.Walters.Comparing Cospan-spans and Tiles via a Hoare-style process calculus.ENTCS 62
[Gad03]F.Gadducci.Term graph rewriting and the pi-calculus.A.Ohori,ed.,APLAS'03
[Gun91]J.Gunawardena.Geometric logic,causality and event structures.CONCUR'91
[HHP93]R.Harper,F.Honsell,G.Plotkin: A Framework for Defining Logics.J.ACM 40(1)
[HL03]F.Honsell,M.Lenisa.Strict Geometry of Interaction Graph Models,LPAR'03
[HL95]F.Honsell,M.Lenisa.Final Semantics for untyped lambda-calculus.TLCA'95
[HMST95]F.Honsell,I.Mason,S.Smith,C.Talcott.A Variable Typed Logic of Effects.Inf.Comput.119(1)
[HO00]M.Hyland,L.Ong.On full abstraction for PCF.Inf.Comput.163
[HS02]F.Honsell,D.Sannella.Prelogical relations.Inf.Comput.178(1)
[JR99]A.Jeffrey,J.Rathke.Towards a theory of bisimulation for local names.LICS'99
[K04]J.Kock.Frobenius algebras and 2D topological Quantum Field Theories.
[KB99]M.Koutny and E.Best.Operational and denotational semantics for the box algebra.TCS 211
[KP04]M.Kick,J.Power.Modularity of Behaviours for Mathematical Operational Semantics.CMCS'04
[KSW04]P.Katis,N.Sabadini and R.F.C.Walters.Compositional minimization in Span(Graph): Some examples. COMETA04
[KSW97]P.Katis,N.Sabadini,R.Walters.Span(Graph): A Categorical Algebra of Transition Systems,AMAST'97
[L04]S.Lack.Composing PROPs.TAC,13
[LPW04]M.Lenisa,J.Power,H.Watanabe.Category theory for operational semantics.TCS 327
[LS04]S.Lack and P.Sobocinski.Adhesive categories.FoSSaCS'04
[Lev80]J.-J.LÈvy.Optimal reductions in the lambda-calculus.
[MPW92]R.Milner,J.Parrow,D.Walker.A calculus for mobile processes.
[MS03]M.Miculan,I.Scagnetto.A Framework for Typed HOAS and Semantics.PPDP'03
[MY05]M.Miculan,K.Yemane.A unifying model of variables and names.FOSSACS'05
[Mes89]J.Meseguer.Conditional rewriting logic as a unified model of concurrency.TCS 96
[Mil03]R.Milner.Bigraphs for petri nets.Lectures on Concurrency and Petri Nets,LNCS 3098
[NPW81]M.Nielsen,G.Plotkin,G.Winskel.Petri Nets,Event Structures and Domains,TCS13
[P80]D.Park.Concurrency and automata on infinite sequences.LNCS 104
[PS93]A.Pitts,I.Stark,Observable properties of higher-order functions that dinamically create local names,or: What's new? MFCS'93
[PT05]J.Power,M.Tanaka.Binding Signatures for Generic Contexts.TLCA'05
[Pal00]C.Palamidessi,ed.,CONCUR'00
[Pal69]P.H.Palmquist.The double category of adjoint squares.LNM 195
[RR88]E.Robinson and G.Rosolini.Categories of partial maps.Info.Comp.79
[RS87]D.E.Rydehard and E.G.Stell.Foundations of equational deductions.CTCS'87
[RSW04]R.Rosebrugh,N.Sabadini and R.F.C.Walters.Symmetric separable algebras in monoidal categories and Cospan(Graph).CT'04
[Ren00]A.Rensink.Bisimilarity of open terms.I&C,156
[Rib96]L.Ribeiro.Parallel Composition and Unfolding Semantics of Graph Grammars.PhD thesis,Technische Universitaet Berlin,1996.
[SNW96]V.Sassone,M.Nielsen,G.Winskel.Models for concurrency: Towards a classification.TCS,170
[SS03]V.Sassone,P.Sobocinski.Deriving Bisimulation Congruences using 2-categories.Nord.J.Comput.10(2)
[SS04]V.Sassone and P.Sobocinski.Locating reaction with 2-categories.TCS,2004.
[SS05a]V.Sassone and P.Sobocinski.A congruence for petri nets.To appear in the Procedings of PNGT'04.,2005.
[SS05]V.Sassone and P.Sobocinski.Reactive systems over cospans.To appear in the LICS'05,2005.
[SW03]N.Sabadini and R.F.C.Walters.Hierarchical automata and P systems.CATS'03
[San96]D.Sangiorgi.A Theory of Bisimulation for the pi-calculus.Acta Inf.33
[Sas96]V.Sassone.An axiomatization of the algebra of Petri net concatenable processes.TCS,170:277-296,1996.
[Sob04]P.Sobocinski.Deriving process congruences from reaction rules,PhD thesis,BRICS,2004.
[Sob05]P.Sobocinski.Process congruences from reaction rules.EATCS Bulletin,2005.
[Str96]R.H.Street.Categorical Structures.Hand.of Algebra (I)
[TP97]D.Turi,G.Plotkin.Towards a Mathematical Operational Semantics.LICS'97
[VSY98]W.Vogler,A.Semenov,A.Yakovlev.Unfolding and finite prefix for nets with read arcs.CONCUR'98
[W87]R.F.C.Walters.The tensor product of matrices.CT'87
Parole Chiave
SISTEMI DI RIDUZIONE; SISTEMI DI TRANSIZIONE ETICHETTATI; CONGRUENZE OSSERVAZIONALI; EQUIVALENZE CONTESTUALI; SPECIFICHE (CO)ALGEBRICHE; SISTEMI APERTI; BIALGEBRE; SEMANTICA DELL'INTERAZIONE; PRINCIPI COINDUTTIVI

Analisi di sistemi di Riduzione mediante sistemi di Transizione (ART)

Università degli Studi di Udine
Abstract
La ricerca di paradigmi generali informatici per comprendere i fenomeni computazionali ha portato in anni recenti ad uno sviluppo impetuoso di formalismi per modellare i più diversi aspetti dei sistemi reattivi e delle loro componenti. Fra le metodologie sviluppate per la specifica e l'analisi di sistemi computazionali distribuiti e concorrenti hanno svolto un ruolo preminente i "sistemi di riduzione" (RS), che permettono di definire gli aspetti dinamici di un sistema di computazione in termini di una famiglia di regole di evoluzione di base, dette regole di riduzione (o di reazione, di riscrittura, ecc).

I sistemi di riduzione tuttavia non descrivono esplicitamente le interazioni tra le differenti componenti di un sistema computazionale. Una comprensione di questi interazioni è spesso fondamentale per la comprensione e l'analisi dei sistemi. Al fine di facilitare l'analisi di proprietà comportamentali, è pratica comune fornire una descrizione delle possibili evoluzioni di un sistema in termini di "sistemi di transizione etichettati" (LTS), ove alle transizioni di stato è associata una osservazione che cattura gli aspetti di interesse della computazione. In particolare, quando l'osservazione caratterizza le possibili modalità di interazione del sistema con l'ambiente circostante viene meno l'esigenza di considerare ogni possibile contesto e l'equivalenza comportamentale può essere definita per il sistema "in isolamento".

Sia per i sistemi a >>>

Coordinatore Scientifico del Programma di Ricerca
Furio HONSELL Università degli Studi di UDINE
Obiettivo del Programma di Ricerca
L'obiettivo generale del progetto è lo sviluppo di strumenti matematici per l'analisi di componenti di sistemi computazionali o agenti computazionali la cui specifica comportamentale sia data in termini di "sistemi di riduzione" ("reduction systems", RS). In generale, il comportamento di tali agenti è definito operazionalmente in termini di regole che descrivono come muta il loro stato, per cui si parla di regole di riduzione, di riscrittura o di firing.

Tale tipo di specifica ha ovvie caratteristiche di naturalità, ed è assai diffusa per modellare caratteristiche di sistemi quali la comunicazione, la concorrenza, la mobilità, la sicurezza. La letteratura sforna in continuazione nuovi approcci che differiscono sia per la nozione di stato (sistemi con topologia ad albero, a grafo, etc.), che per le tecniche di applicazione delle regole.

Particolarmente significativo per la riscrittura di (sistemi computazione descritti come) grafi è l'approccio basato sulla costruzione del "doppio pushout" (DPO) e sulla ricca teoria categoriale sottesa [EEKMG97]. Il suo successo ha spinto la ricerca di opportune generalizzazioni di tale costruzione. Un caso emblematico è rappresentato dagli "High-Level Replacement Systems" (HLRS), nati con l'obiettivo di fornire una caratterizzazione della categoria ambiente sulla quale eseguire la riscrittura, che assicuri la validità dei risultati più significativi ottenuti sui grafi, quali i teoremi di >>>

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
Come già menzionato nella parte dedicata agli obiettivi del progetto, un importante e flessibile formalismo per descrivere la computazione è costituito dai sistemi di riduzione (RS). Questo formalismo però ha l'evidente svantaggio di mancare di composizionalità, ossia il comportamento di una componente non è riconducibile al comporamente delle sue componenti.
Un modo per ottenere una descrizione composizionale è utilizzare formalismi che definiscano esplicitamente per ogni componente come questi può interagire con il resto del sistema. Un esempio di questi, preso in particolare attenzione dal progetto, è costituito dai Sistema di Transizione etichettati (LTS). Negli LTS, le etichette permettono di dare una descrizione della comunicazione sulle interfacce di ogni componente. Inoltre negli LTS è possibile fare astrazioni sulle componenti, rispetto al loro comportamento sui confini, attraverso la nozione di bisimilarità introdotta in [Par80].

Recentemente, in [LM00] è stato proposto un approccio generale che, dato un RS, permette di definire un LTS per il quale la nozione di bisimilarità risulti una congruenza. Tale approccio si basa su una costruzione detta "pushout relativo" (RPO), in seguito generalizzato da [SS02] al concetto 2-categoriale di "grupoidal RPO" (GRPO). L'idea principale è che le etichette associate ad una componente sono definite dai contesti minimali nel quale la componente può evolvere. Già nella teoria del lambda calcolo era >>>