RICERCA ITALIANA     

Automi e Linguaggi Formali: aspetti matematici e applicativi

Università degli Studi di Palermo

Abstract

Il progetto si propone di far avanzare la conoscenza della teoria degli automi e la sua applicabilità a problemi scientifici e tecnologici.
La ricerca utilizzerà sia approcci classici, come la combinatoria e i semigruppi, sia nuovi strumenti concettuali dell'algebra non commutativa, della logica, della teoria della probabilità e della dinamica simbolica. Potenziali applicazioni scientifiche includono fra le altre, la codifica, la biologia, le scienze cognitive e neurologiche, la compilazione e la verifica del software, le risorse del web.
La cooperazione interdisciplinare fra matematici, informatici teorici e ingegneri permetterà una sinergia tra la ricerca fondamentale e lo studio di nuovi modelli formali orientati alle applicazioni.
In uno scenario dove un gruppo di scienziati qualificato e di studenti di dottorato può comunicare e condividere sia le sfide provenienti da nuove applicazioni della teoria degli automi, sia le intuizione teoriche, questo programma catalizzerà progressi in entrambe le direzioni.
Evitando dispersioni sull'intero settore, sarà affrontato un campo limitato di direzioni di ricerca.


A1) Modelli di Automi, serie formali, e loro proprietà
Studio di modelli computazionali quali gli automi quantistici, mediante l'analisi dei loro comportamenti descritti da linguaggi formali. Studio della complessità descrizionale di automi con vincoli di risorse. Proprietà algebriche di automi a stati finiti, con particolare attenzione allo studio mediante automi di semigruppi inversi. Studio di proprietà di serie formali razionali e olonomiche, con applicazioni alle statistiche di pattern e al conteggio e generazione casuale di parole in linguaggi di date classi.

A2) Codici, combinatoria su parole e strutture complesse.
Applicazioni della combinatoria delle parole alla Compressione Dati, allo string matching approssimato, al Fragment Assembly Problem.
Proprietà combinatorie, aritmetiche e strutturali delle parole Sturmiane.
Proprietà d'ordine di classi di strutture quali cammini, permutazioni e partizioni.
Problemi di enumerazione di permutazioni a motivo escluso.
Caratterizzazione dei codici fattorizzanti mediante loro descrizione strutturale.
Condizioni di decifrabilità più debole; Varietà di codici.

A3) Grammatiche context-free e rappresentazioni non convenzionali di linguaggi formali.
Grammatiche XML e linguaggi XML.
Miglioramento di costruzioni classiche di traduttori syntax-directed per linguaggi deterministici.
Nuove estensioni del teorema di Higman.
Problemi di base e algoritmici delle descrizioni basate su linguaggi associativi (Associative Language Descriptions, ALD); il problema aperto dell'inclusione dei regolari nella classe dei linguaggi ALD.
Caratterizzazione dei linguaggi regolari generati dai sistemi finiti di splicing (lineare o circolare).

A4) linguaggi e strutture bidimensionali
Studio di modelli formali recenti che estendono a due dimensioni le classiche definizioni di linguaggi Regolari e Context-Free. Più precisamente per i Tiling Systems (TS) e le Tile Rewriting Grammars (TRG), ricerca sugli automi corrispondenti e algoritmi di parsing, relazioni con altri modelli, generalizzazione di espressioni regolari a due dimensioni, caratterizzazioni di linguaggi unari, applicabilità ad analisi di immagini.
Studio di alcune estensioni di polyomini L-convessi negli ambiti di ricerca classici della teoria dei polyomini.

A5) Modelli formali di sistemi distribuiti e temporizzati.
La ricerca su modelli di automi adatti alla verifica e all'analisi di sistemi, in paricolare su:
Automi temporizzati ed estensioni a macchine con memoria illimitata, come quelle dotate di stack e gli automi dense counter; problemi di complessità rilevanti per il model checking. Ricerca su algoritmi per la parallelizzazione del codice per programmi rappresentati da modelli formali, cioè linguaggi traccia, e mediante trasformazioni affini. <<<

Coordinatore Scientifico del Programma di Ricerca

Antonio RESTIVO Università degli Studi di PALERMO

Obiettivo del Programma di Ricerca

La Teoria degli automi (AT) è una delle aree dell'informatica affermate da più lungo tempo. Negli ultimi anni, la AT non solo si è sviluppata in molte direzioni diverse, ma si è anche evoluta a vari livelli: l'esplorazione di nuovi modelli ed applicazioni ha, nello stesso tempo, stimolato una grande varietà di profonde teorie matematiche. Più azioni coordinate svilupperanno la conoscenza della AT e la applicabilità a difficili problemi scientifici e tecnologici.
Applicazioni standard in informatica della AT includono fra le altre, la compilazione e la verifica del software. Negli ultimi anni nuove applicazioni di concetti della AT sono emerse dalla biologia, dalla fisica, dalle scienze neuro-cognitive, dalla tomografia, dalla linguistica, etc., mentre gli sviluppi della tecnologia informatica hanno incrementato il bisogno di una progettazione formale e di metodi di verifica per far fronte problemi come la sicurezza e i servizi delle reti e le risorse del web. La lista non è esaustiva, poiché la AT ambisce a rivolgersi verso nuove applicazioni, come l'analisi di immagini, uno dei punti principali di questo progetto.
Nello stesso tempo, le basi matematiche della AT si trovano in settori della matematica sempre più avanzati. Mentre nei primi anni sessanta era sufficiente la sola teoria dei grafi elementare e la combinatoria, ultimamente sono stati introdotti con successo nuovi strumenti provenienti dall'algebra non commutativa, dalla logica, dalla teorie della probabilità e della dinamica simbolica.
Entrambe le tendenze hanno valorizzato il ruolo della ricerca fondamentale in AT e sottolineato l'importanza di un'interazione più stretta fra scienziati teorici ed applicativi.
Da un lato, gli sviluppi significativi negli aspetti fondamentali della AT possono essere misurati dai recenti progressi su alcuni profondi problemi aperti della teoria classica. D'altra parte, nuovi problemi teorici vengono fuori dalle applicazioni e anche dal nascere di nuovi modelli di automi e di meccanismi generativi, motivati dalle applicazioni, che richiedono un'investigazione sistematica dei loro aspetti teorici.
Questo progetto è un programma multidisciplinare all'incrocio fra matematica, informatica teorica ed applicazioni. In uno scenario dove scienziati qualificati e studenti di dottorato comunicano e condividono sia le sfide provenienti da nuove applicazioni della AT, sia le intuizione teoriche, il
programma catalizzerà progressi in entrambe le direzioni. Questo progetto è sinergico con il programma quinquennale dell'European Science Foundation chiamato AutoMathA, che è stato proposto con successo da alcuni membri del nostro gruppo. Questa iniziativa darà delle opportunità per la comunicazione scientifica e la collaborazione con i principali gruppi europei del campo, amplificando l'impatto potenziale della nostra ricerca.
Al fine di evitare una dispersione sull'intero campo, questo progetto si focalizzerà su poche importanti direzioni di ricerca:
A1) Modelli di Automi, serie formali, e loro proprietà
A2) Codici, combinatoria su parole e strutture complesse
A3) Grammatiche Context Free e rappresentazioni non convenzionali di linguaggi formali
A4) Linguaggi e strutture bidimensionali
A5) Modelli formali di sistemi distribuiti e temporizzati
Per ognuna di queste direzioni, descriviamo sinteticamente il contenuto, gli obiettivi e gli approcci che intendiamo sviluppare. Tali aspetti saranno presentati in modo più dettagliato nelle sezioni successive.
A1) Modelli di Automi, serie formali, e loro proprietà
Gli Automi sono uno strumento per modellizzare sistemi reali; la loro analisi richiede metodi algebrici (per esempio teoria dei semigruppi, serie formali) e i risultati su automi possono avere implicazioni in Algebra.
In particolare diverse proprietà degli automi possono essere investigate mediante le serie formali in variabili (non)commutative. Le ricerche si baseranno su modelli e proprietà di automi quantistici, su alcune recenti relazioni fra la AT e la teoria dei semigruppi, sull'analisi della complessità descrizionale di automi con vincoli di risorse, sulle applicazioni di tecniche che coinvolgono serie di potenze formali alla statistica dei pattern e alla generazione casuale di parole in un linguaggio.
A2) Codici, combinatoria delle parole e delle strutture complesse.
La ricerca sarà focalizzata su problemi di base e algoritmici, guardando anche agli aspetti applicativi. Per esempio, saranno analizzate proprietà combinatorie, strutturali e aritmetiche di parole speciali (come quelle Sturmiane). Saranno studiate proprietà combinatorie della trasformata di Burrows-Wheeler, anche in relazione alla bioinformatica e alla compressione dati.
Studieremo proprietà d'ordine di classi di strutture quali cammini, permutazioni e partizioni e possibili applicazioni del metodo ECO a problemi di enumerazione di permutazioni a motivo escluso. Per quanto riguarda i codici a lunghezza variabile, affronteremo la famosa, ancora aperta, congettura della fattorizzazione di Schutzenberger. Studieremo condizioni di decifrabilità più deboli dell'unica decifrabilità, seguendo l'approccio di Guzman basato sulla nozione algebrica di varietà.
A3) Grammatiche context-free e rappresentazioni non convenzionali di linguaggi formali.
La struttura dei documenti XML è definita da una grammatica context-free, detta grammatica XML. Si studieranno le proprietà formali dei corrispondenti linguaggi generati (linguaggi XML), cercando estensioni e tecniche per problemi legati a tipiche applicazioni in ambito XML.
Per quanto riguarda la traduzione syntax-directed (SDT), si cercherà di schematizzare e sfoltire il campo degli algoritmi tradizionali per linguaggi context-free deterministici.
Da un punto di vista più teorico, si cercheranno nuove estensioni del Teorema di Higman.
Associative Language Descriptions (ALD) è una grammatica non generativa che usa le associazioni in luogo dei simboli non terminali. Saranno affrontati problemi di base e algoritmici, quale quello dell'inclusione dei regolari nella classe dei linguaggi ALD.
Sarà studiato il potere computazionale dei sistemi splicing finiti (lineari o circolari).
A4) Linguaggi e strutture bidimensionali
Il primo obiettivo del nostro lavoro consiste nello studio e nella descrizione completa della classe REC dei linguaggi bidimensionali riconoscibili con la loro caratterizzazione per mezzo di un modello di automa più vicino al modello classico per i linguaggi di sequenze. Studieremo anche le generalizzazioni delle grammatiche context-free da 1D a 2D, in particolare delle grammatiche Tile Rewriting (TRG) in relazione alle sue possibili applicazioni.
Una linea di ricerca parallela affronterà problemi legati ai polyomini, con particolare attenzione a generalizzazioni degli L-convessi, come l'enumerazione e il tassellamento. Nell'ambito della tomografia discreta si vuole analizzare la ricostruzione di un oggetto fisico dalle proiezioni con assorbimento.
A5) Modelli formali di sistemi distribuiti e temporizzati
Analisi e verifica di sistemi. Lo scopo principale è risolvere problemi di decisione per vari modelli a stati infiniti, e in particolare su automi a stati finiti estesi con contatori, come il modello DCA. I problemi da studiare sono orientati alle applicazioni alla verifica formale di sistemi.
Compilazione e parallelizzazione. L'obiettivo principale è modellare la schedulazione e la parallelizzazione di programmi sotto forma di stringhe su alfabeti parzialmente commutativi ("tracce"). Ciò tuttavia richiede di approfondire i fondamenti teorici dei linguaggi traccia.
Modelli per il web
L'obiettivo è studiare, usando catene di Markov ergodiche, varianti di PageRank più robuste rispetto al link spam, oltre a sviluppare algoritmi per indicizzare e interrogare documenti raccolti dal web. <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

La Teoria degli Automi e dei Linguaggi Formali è un ampio e ancora in crescita corpo di conoscenze. I risultati classici ed i più recenti sviluppi di tale teoria sono raccolti in [RoSa]. La base di partenza scientifica relativa ai temi delle ricerche proposte viene data nel seguito riferendosi ai punti del programma riportati nella Sezione 2.1.

A1)Modelli di Automi, serie formali, e loro proprietà.
A partire dal lavoro di Rabin e Scott, gli automi sono stati oggetto di studi di ampio spettro, con contributi in aree dalle architetture di calcolo all'algebra. Richiamiamo qui alcune recenti estensioni del modello di automa al caso quantistico, alcune recenti interazioni tra la teoria degli automi e lo studio di strutture algebriche, contributi in ambito di complessità descrizionale, l'uso di tecniche di manipolazione con serie formali quali quelle olonomiche per problemi di conteggio e generazione casuale.
Fra le recenti estensioni, vanno segnalati i vari modelli di automi quantistici a stati finiti [BC,KW]. Proprietà di questi modelli sono utili per indagare i vantaggi computazionali dell'interferenza quantistica. Ci sono analogie col caso probabilistico; per esempio, Rabin ha provato che i comportamenti di automi con taglio isolato sono esattamente i linguaggi regolari; via proprietà di serie formali, questo risultato può essere esteso a numerosi modelli di automi quantistici [BMP]. Per altre proprietà, gli automi quantistici esibiscono profonde differenze; ad esempio, mentre per automi probabilistici è indecidibile se un taglio è isolato [BMT], sorprendentemente per automi quantistici tale problema è decidibile[DJK]. La teoria degli automi ha feconde applicazioni nello studio di proprietà di struttura algebriche. Ad esempio varie questioni di decidibilità [CMP] sono ottenute facendo uso della nozione di automa di Schützenberger di una parola w rispetto ad una data presentazione. Al contrario, gli approcci algebrici sono fondamentali per chiarire proprietà in teoria degli automi. Ad esempio, detto k-comprimibile un automa finito per il quale la cardinalità dell'immagine dell'insieme degli stati sotto l'azione di una parola w si riduca di k, le parole che 2-comprimono ogni automa 2-comprimibile, sono state caratterizzate in termini di proprietà di sottogruppi di particolari gruppi liberi [AC].
Nell'ambito della teoria degli automi, una naturale misura di complessità descrizionale è il numero di stati; risultati in questa area possono avere profonde ricadute in alcune fondamentali questioni aperte in complessità strutturale [SS]. Numerosi risultati hanno evidenziato il potere descrizionale di estensioni (two-way, alternanti, probabilistici, quantistici). Particolarmente interessante è il caso degli automi unari, in cui sono evidenziate dissimmetrie col caso generale [MP].
L'obiettivo di una statistica di pattern è di determinare la frequenza con la quale una parola (pattern) compare in un testo generato a caso secondo modelli probabilistici come quelli Bernoulliani, Markoviani e razionali (definiti a partire da automi a stati finiti pesati [BCGL]). Questa problematica è di grande interesse nell'analisi di sequenze di DNA.
La classe delle serie formali olonomiche è stata recentemente oggetto di numerosi studi con applicazioni in ambito di manipolazione simbolica. L'individuazione di classi di linguaggi con funzioni generatrici olonomiche ha permesso lo sviluppo di algoritmi efficienti per il conteggio e la generazione casuale di parole [MR].

A2) Codici, combinatoria delle parole e delle strutture complesse.
La combinatoria delle sequenze finite o infinite di simboli appartenenti a un alfabeto finito ha avuto negli ultimi anni un considerevole sviluppo con numerose applicazioni in vari campi quali l'Algebra, la Fisica e la Biologia Molecolare [Lot1,Lot2]. La maggior parte dei risultati della teoria degli automi e dei linguaggi formali fa uso delle proprietà combinatorie delle parole [CK]. Un interessante approccio consiste nello studio di problemi inversi, quale quello di determinare univocamente una parola dato un conveniente insieme di suoi fattori. Ad esempio in [MReS2] è stato provato che l'insieme dei fattori proibiti minimali di una parola (finita o infinita) assume un ruolo fondamentale nel determinare la struttura della parola stessa e, nel caso finito, esso permette di ricostruire in tempo lineare la parola stessa. I risultati ottenuti si applicano a problemi di natura biologica, come per esempio il Fragment Assembly Problem. Complementare a questo tipo di ricerca è lo studio delle "ripetizioni" in una parola. In particolare, lo studio dei cosiddetti "fattori speciali" ha permesso di associare ad ogni parola alcuni parametri caratteristici che forniscono molta informazione sulla sua struttura, introducendo alcune generalizzazioni della nozione di parola periodica.
Le numerose proprietà combinatorie di cui godono le parole Sturmiane hanno conferito loro un ruolo importante [BedL], giustificando l'esistenza di varie definizioni equivalenti e di vari teoremi di struttura [CdL]. L'origine di tali parole è da ricercare in un lavoro del 1772 dell'astronomo Bernoulli, ma il primo studio sistematico risale agli anni '40 [MoH].
Lo studio combinatorico delle sequenze trova diverse applicazioni in numerosi e svariati campi di ricerca. In Compressione Dati per esempio, nel 1994 M. Burrows e D. Wheeler hanno introdotto una trasformazione reversibile su parole che permuta il testo in modo da renderlo più facilmente comprimibile anche mediante semplici algoritmi di compressione [BW]. La trasformata di Burrows-Wheeler (nota ormai come BWT) rappresenta ad esempio il cuore dell'algoritmo BZIP2 che è diventato lo standard per la compressione lossless [S]. Studi recenti hanno messo in evidenza interessanti proprietà combinatoriche della BWT. In particolare, in [MaReS1] è stato provato che le parole Sturmiane standard caratterizzano il caso estremale della BWT nel caso di alfabeti binari. In [ChDPe] è stato dimostrata una stretta connessione tra la BWT e un noto risultato di combinatoria delle permutazioni [GeR]. Ciò ha consentito di definire una nuova trasformata che estende la BWT a più parole [MaReS2].
Strettamente connessa con la problematica della combinatoria delle parole è quella relativa ai codici. Essa trae origine dai primi lavori di Shannon sulla Teoria dell'Informazione ed è stata in seguito sviluppata secondo un approccio algebrico dalla scuola francese di M.P.Schutzenberger in stretta connessione con la teoria dei Linguaggi Formali [BerP]. Alcuni problemi fondamentali della teoria dei codici sono ancora aperti, come la congettura della fattorizzazione di Schutzenberger. In uno dei migliori risultati parziali ottenuti viene dimostrata una importante proprietà algebrica dei codici massimali finiti molto vicina a quella proposta [Re]. Dimostrazioni della validità della congettura per alcune famiglie significative di codici sono contenute in [DF,PS,ZG]. Più recentemente alcune applicazioni hanno suggerito l'introduzione di nozioni più deboli di quelle di codice univocamente decifrabile, quale quella di codice Multiset Decifrabile (MSD). In [Guz] si introduce il concetto di decifrabilità di un codice in un monoide e quello conseguente di varietà di codici. In [BRe] si è dimostrato che i codici UD (univocamente decifrabili) costituiscono la varietà caratterizzata dal fatto di soddisfare la disuguaglianza di Kraft-McMillan.
La combinatoria enumerativa e la generazione esaustiva e casuale costituiscono linee di ricerca che si complementano e si integrano con la teoria dei linguaggi bidimensionali e la teoria dei codici. Uno degli strumenti più utilizzati per ricerche in combinatoria enumerativa è il cosiddetto modello delle parole: esso consiste nella codifica delle istanze o delle soluzioni di un problema tramite parole di un dato linguaggio. Principalmente, i linguaggi regolari e context-free permettono formalizzazioni di rilevante interesse combinatorio. Per essi è stata introdotta la metodologia di Schützenberger [Sch] che permette di enumerare le parole del linguaggio stesso secondo vari parametri. La teoria delle strutture decomponibili e il metodo ECO ([BaDLPP]) sono strumenti più prossimi agli oggetti combinatori piuttosto che la loro codifica tramite un linguaggio [BaDLPP]. La generazione casuale di strutture combinatorie (alberi, grafi, poliomini o altre strutture planari discrete) è diventata un argomento importante in Informatica. Attualmente i metodi di generazione più usati sono basati sui codici Gray per le buone prestazioni degli algoritmi che li utilizzano [Sav].

A3) Grammatiche context-free e rappresentazioni non convenzionali di linguaggi formali.
Le grammatiche context-free costituiscono il modello classico utilizzato nella descrizione della sintassi dei linguaggi di programmazione e hanno avuto un ruolo centrale nella tecnologia dei compilatori. Più recentemente, le grammatiche context-free sono state utilizzate per descrivere documenti XML. L'XML (eXtensible Murkup Language) è uno degli strumenti oggi più diffuso per scambiare informazioni su Web e la struttura dei documenti XML può essere descritta da DTD (Documents Type Definitions), una grammatica context-free deterministica, detta grammatica-XML, che genera un cosiddetto linguaggio-XML. In [BB] viene proposta una caratterizzazione di tali linguaggi e viene studiata la decidibilità di alcuni problemi relativi ai linguaggi-XML.
Per ciò che riguarda invece il progetto di compilatori, lo stato dell'arte nelle traduzioni guidate dalla sintassi (SDT) è ormai stabile da anni probabilmente perchè fin dagli anni '60 le esigenze pratiche fondamentali hanno trovato risposta negli algoritmi di parsificazione (LL(k) and LR(k)). La spinta per migliorare l'assetto teorico di questa materia si è affievolita, ma il progresso appare ancora possibile.
In un contesto più teorico, sono stati ottenuti notevoli risultati, sia di natura algebrica che algoritmica, riguardanti la funzione di crescita e di struttura dei linguaggi context-free. Altri risultati riguardano l'individuazione di condizioni di regolarità per classi particolari di linguaggi context-free. Alcune di esse sono basate sulla nozione di "well quasi order", che costituisce una naturale estensione di quella classica di buon ordine parziale e che è stata ampiamente studiata nella teoria dei linguaggi formali [dLV,EHR,Hi].
Vicine per alcuni aspetti alle grammatiche context-free sono alcune rappresentazioni non convenzionali di linguaggi formali, recentemente introdotte.
Ad esempio, le Associative Language Descriptions (ALD), introdotte in [CPS], si distinguono dalle grammatiche context-free perchè non usano simboli nonterminali per contraddistinguere le classi sintattiche, seguendo un approccio che si ispira ai comportamenti associativi della corteccia cerebrale. I linguaggi definiti da ALD sono strettamente contenuti nei CF, ma in pratica si è trovato che i linguaggi di interesse applicativo sono trattabili con ALD. Tuttora aperto è il problema se i linguaggi regolari siano inclusi nella famiglia ALD, pur se molte sottofamiglie regolari lo sono.
I sistemi di splicing e i sistemi a membrana (P-sistemi) sono sistemi di riscrittura ispirati da fenomeni di biologia molecolare. L'analisi della potenza computazionale di tali sistemi è svolta con strumenti della teoria dei linguaggi formali. Solo per alcune classi di linguaggi definite da tali formalismi sono noti risultati di caratterizzazione e proprietà di chiusura [HPP,PA].

A4) Linguaggi e Strutture bidimensionali
Circa 40 anni fa Minsky suggerì (cf.[Mi]) che le immagini potevano essere considerate come frasi di un linguaggio bidimensionale, a cui sia possibile estendere i formalismi sviluppati nell'ambito della teoria dei linguaggi formali. Importanti in questo contesto sono gli approcci in termini di grammatiche [Ro] e di automi [BH,IT]. Più recentemente sono stati proposti nuovi approcci formali, per una sintesi vedi [GR]. Prendendo spunto da idee e problemi combinatorici sulle stringhe, si è cercato di estendere alcuni risultati e tecniche alle strutture bidimensionali. Proposte recenti sono le espressioni regolari a 2D, i Tiling Systems (TS), e le grammatiche Tile Rewriting (TRG) [CP]. Le TRG rappresentano una buona generalizzazione sia delle grammatiche CF a 1D, che dei tiling systems. Di recente è stato studiato un algoritmo polinomiale di parsificazione per TRG, generalizzando il classico algoritmo CKY per le grammatiche CF. Tra i vari problemi aperti vi è quello di trovare una descrizione soddisfacente di REC (famiglia dei linguaggi bidimensionali riconoscibili secondo la definizione data in [GR]) in termini di espressioni regolari. Sono state caratterizzate in [AGM] alcune sottofamiglie di REC in termini di espressioni regolari.
Una linea di ricerca sviluppata nell'ambito delle strutture bidimensionali ha come oggetto i polyomini, intesi come unione finita di celle elementari del piano discreto. Essi sono stati studiati approfonditamente da Golomb nel 1965 [Go] e costituiscono un'utile esemplificazione di modelli di fenomeni fisici e chimici. Un problema di ricerca largamente affrontato consiste nella ricostruzione di polyomini a partire da un numero finito di proiezioni. Ciò ha importanti risvolti nell'ambito della Tomografia Discreta [HK]. Per l'esemplificazione del problema sono state introdotte famiglie di polyomini che soddisfano proprietà di convessità. In [CR1] è stata introdotta la famiglia degli L-convessi. Essi sono univocamente individuati dalle loro proiezioni orizzontali e verticali sia nel caso discreto che continuo[CFRR2]. Generalizzando al caso 2D il teorema di Higmann sulle parole, si è provato che essi sono un well-ordering [CR2]rispetto all'ordine di subpicture introdotto da Matz.Da un punto di vista enumerativo, è nota la funzione generatrice dei polyomini convessi rispetto al perimetro ed è algebrica [DV], mentre quella degli L-convessi è razionale[CFRR1].

A5) Modelli formali di sistemi distribuiti e temporizzati
La teoria degli automi è di grande rilevanza per la verifica automatica di applicazioni distribuite e temporizzate. Per es, il model checking (MC) consente,a partire da specifiche espresse in logica temporale, di verificare automaticamente se la specifica è valida sull'implementazione a stati finiti.Gli automi alternanti consentono di definire algoritmi di MC efficienti [V]. Gli automi temporizzati (TA) [AD] sono un naturale modello per i sistemi in tempo reale, e consentono alcune attività di MC.In [GDIS,IDS] è stato proposto un modello per la analisi di TA e sistemi ibridi, detti Dense Counter Automata (DCA), consentendo contatori e nastro d'ingresso a valori reali.
Nell'ambito dello studio dei modelli e algoritmi per il web, le ricerche più rilevanti si sono concentrate sulle trasformazioni di codice per parallelizzare i cicli [BGS,WL]. Un nuovo approccio cerca di applicare i cosiddetti linguaggi traccia, un modello formale della concorrenza fondato su monoidi parzialmente commutativi. I principali risultati della teoria delle tracce sono sintetizzati nel libro [DR].
Il problema del web ranking riguarda l'ordinamento dei risultati, forniti da un motore di ricerca, di una query relativa al grafo Web. Studi rilevanti hanno considerato strategie di visita per toccare per prime pagine con alto PageRank [NW],modelli di grafo che "assomiglino" a veri grafi del Web [BKM], algoritmi efficienti per raccogliere, indicizzare e comprimere grandi "snapshot" del Web [WMB,CM,BV]. <<<