Logica temporale
tempo fa (ma tanto tempo fa...) mi sono occupata di logica temporale. all'epoca ho trovato enormità di materiale sulla logica del tempo lineare e solo qualche articolo sulla logica del tempo ramificato. ho ripreso un articolo che era vecchio già allora (di un certo Leslie Lamport, "sometime is sometimes not never", mi pare del 1980) e l'ho utilizzato per approfondire l'argomento "modalità" nei sistemi che ho chiamato "puramente temporali". all'epoca non c'era tutta questa opportunità di scambiarsi opinioni ed informazioni. recentemente ho cercato in Internet qualcosa sull'argomento, ed ho trovato ancora riproposto lo stesso articolo. se qualcuno è al corrente di recenti sviluppi.... io sarei curiosa di sapere se le mie vecchie ricerche sono state utilizzate (è difficile, dato che erano a conoscenza di una ristretta cerchia di persone), se si è arrivati comunque a risultati simili o alternativi da parte di "altri" ricercatori, oppure se sono "morte nel cassetto" (in tal caso mi farebbe piacere sapere se, rispolverate, sono ancora utili oppure del tutto superate). ora ho pochissimo tempo, ma prossimamente potrei mandare a voi qualche informazione in più. che ne pensate?
per il momento gradirei sapere se c'è tra voi qualche specialista dell'argomento. grazie dell'attenzione. ciao.
per il momento gradirei sapere se c'è tra voi qualche specialista dell'argomento. grazie dell'attenzione. ciao.
Risposte
Ciao Ada, grazie per le indicazioni.
Io sono un mediocre informatico, mi occupo da molti anni di software critico per sistemi embedded in tempo reale, la LTL di Manna & Pnueli è uno dei vari strumenti che utilizziamo per la specifica e la verifica semiautomatica. Purtrroppo ho perso i contatti con il mio boss, da qualche anno... la cosa però non mi stupisce troppo, è sempre stato un misantropo bizzarro con l'abitudine di sparire per lunghi periodi, uno che veniva in azienda (una multinazionale...) vestito in braghettoni e sandali alla Jeffrey "Drugo" Lebowski ne "Il grande Lebowski", parlava come il Benigni e ci leggeva paginate di Calvino e Musil durante i corsi di formazione alla programmazione embedded critica, non so se mi spiego.
Matto come un cavallo, ma se ho mai conosciuto uno che rischia di prendere il Turing Award direttamente dalle mani di Dana Scott, non c'è dubbio: è lui.
Dopo la tua descrizione, sono sempre più convinto di non aver visto "in giro", nella letteratura applicativa, materiale specifico sulla BTL "puramente temporale" con cinque modalità e senza operatore Next. Questo naturalmente non esclude che vi siano nicchie di interesse accademico attorno all'argomento, ma di certo non si tratta di un metodo al centro dell'attenzione nella comunità dei practitioners della quale mi capita di far parte.
Io sono un mediocre informatico, mi occupo da molti anni di software critico per sistemi embedded in tempo reale, la LTL di Manna & Pnueli è uno dei vari strumenti che utilizziamo per la specifica e la verifica semiautomatica. Purtrroppo ho perso i contatti con il mio boss, da qualche anno... la cosa però non mi stupisce troppo, è sempre stato un misantropo bizzarro con l'abitudine di sparire per lunghi periodi, uno che veniva in azienda (una multinazionale...) vestito in braghettoni e sandali alla Jeffrey "Drugo" Lebowski ne "Il grande Lebowski", parlava come il Benigni e ci leggeva paginate di Calvino e Musil durante i corsi di formazione alla programmazione embedded critica, non so se mi spiego.
Matto come un cavallo, ma se ho mai conosciuto uno che rischia di prendere il Turing Award direttamente dalle mani di Dana Scott, non c'è dubbio: è lui.
Dopo la tua descrizione, sono sempre più convinto di non aver visto "in giro", nella letteratura applicativa, materiale specifico sulla BTL "puramente temporale" con cinque modalità e senza operatore Next. Questo naturalmente non esclude che vi siano nicchie di interesse accademico attorno all'argomento, ma di certo non si tratta di un metodo al centro dell'attenzione nella comunità dei practitioners della quale mi capita di far parte.
non è prevedibile una generalizzazione, anche perché dipende dal significato (semantico) da attribuire ai singoli operatori. sulla LTL si trovano diversi sistemi con diverso numero di modalità. quello preso in considerazione da me ne ha 5, il sistema S4 di Lewis ne ha 7, per il sistema DX di Pnueli non si può fare un discorso analogo data la presenza dell'operatore next che porta all'infinito le modalità.
io me ne sono occupata nel 1989 (quando ho cercato disperatamente l'articolo del 1980 di Lamport: "sometime is sometimes not never...") e nel periodo immediatamente successivo (90-91), e, nonostante una bibliografia sostanziosa della tesi ed altre ricerche successive, non ho trovato praticamente nulla sulla BTL. gli argomenti collegati sono molti, ma il sistema di modalità con il significato di puramente temporale è preciso e rigido, non si offre a "piccole variazioni".
spero di essere stata chiara.
se vuoi un'idea degli argomenti collegati, do uno sguardo all'indice della tesi e una sfogliata, per segnalare delle cose qua e là:
concorrenza: mutua esclusione, proprietà safety e liveness, calcolabilità e congetture (problema aperto: livello di comlessità-espressività del linguaggio delle specifiche di Lamport).
logica temporale: studio di diversi sistemi e costruzione di BT e LT; problemi connessi (regole di semplificazione e algoritmo di riscrittura, espressività delle modalità e problema probabilistico, completezza del reticolo delle modalità e problema topologico), problema aperto (topologico).
conclusioni e problemi aperti: gerarchie, proprietà safety e liveness, operatori binari.
spero di aver risposto adeguatamente: se ti interessa qualche argomento in particolare ora forse sai che cosa chiedere.
tu di che cosa ti occupi? senti ancora il tuo vecchio capo?
a risentirci su questo forum. ciao.
io me ne sono occupata nel 1989 (quando ho cercato disperatamente l'articolo del 1980 di Lamport: "sometime is sometimes not never...") e nel periodo immediatamente successivo (90-91), e, nonostante una bibliografia sostanziosa della tesi ed altre ricerche successive, non ho trovato praticamente nulla sulla BTL. gli argomenti collegati sono molti, ma il sistema di modalità con il significato di puramente temporale è preciso e rigido, non si offre a "piccole variazioni".
spero di essere stata chiara.
se vuoi un'idea degli argomenti collegati, do uno sguardo all'indice della tesi e una sfogliata, per segnalare delle cose qua e là:
concorrenza: mutua esclusione, proprietà safety e liveness, calcolabilità e congetture (problema aperto: livello di comlessità-espressività del linguaggio delle specifiche di Lamport).
logica temporale: studio di diversi sistemi e costruzione di BT e LT; problemi connessi (regole di semplificazione e algoritmo di riscrittura, espressività delle modalità e problema probabilistico, completezza del reticolo delle modalità e problema topologico), problema aperto (topologico).
conclusioni e problemi aperti: gerarchie, proprietà safety e liveness, operatori binari.
spero di aver risposto adeguatamente: se ti interessa qualche argomento in particolare ora forse sai che cosa chiedere.
tu di che cosa ti occupi? senti ancora il tuo vecchio capo?
a risentirci su questo forum. ciao.
Andando ad orecchio, perché al momento non ho accesso ai motori di ricerca delle pubblicazioni con referee, posso darti qualche riferimento su CTL e CTL*, ossia le Computational Tree Logics che costituiscono l'evoluzione della BTTL della tua tesi, forse con qualche minimo aggiustamento assiomatico. Se ne sono occupati negli anni i soliti Clarke, Grumberg, Emerson, Halpern, Lei dopo i lavori "seminali" del trio Ben-Ari, Manna, Pnueli nei primissimi anni '80.
Non conosco la situazione della ricerca accademica in materia (e condivido appieno le tue perplessità su tale mondo: non me ne voglia il buon Fioravante), ma da un punto di vista applicativo le logiche branching hanno numerosi difetti che ne hanno determinato lo scarso successo a livello industriale, e quindi uno scarso interesse a studiarne a fondo le proprietà. Prima di tutto, la scarsa leggibilità: per casi non banali il metodo branching rischia di diventare meno leggibile del codice in un linguaggio di programmazione, il che lo rende ontologicamente inutile ! Inoltre CTL è veramente poco applicabile in fase di verifica: la complessità computazionale di tale approccio nella dimostrazione del contenimento delle tracce in sistemi con numero finito di transizioni è dimostrabilmente PSPACE-completa. Ma questo nella pratica sembra limitare l'uso di CTL solo alla fase di specifica, lasciando spazio alla LTL per la verifica.
Curiosità: nella tua dimostrazione, oltre a provare che la tua logica ammette esattamente 25 modalità distinte, avevi generalizzato la relazione tra il numero di operatori e il conteggio totale delle modalità distinte ? Ovvero una risposta a domande come "Cosa succederebbe con sei operatori ? E con un N arbitrario (ovviamente finito) ?".
Non conosco la situazione della ricerca accademica in materia (e condivido appieno le tue perplessità su tale mondo: non me ne voglia il buon Fioravante), ma da un punto di vista applicativo le logiche branching hanno numerosi difetti che ne hanno determinato lo scarso successo a livello industriale, e quindi uno scarso interesse a studiarne a fondo le proprietà. Prima di tutto, la scarsa leggibilità: per casi non banali il metodo branching rischia di diventare meno leggibile del codice in un linguaggio di programmazione, il che lo rende ontologicamente inutile ! Inoltre CTL è veramente poco applicabile in fase di verifica: la complessità computazionale di tale approccio nella dimostrazione del contenimento delle tracce in sistemi con numero finito di transizioni è dimostrabilmente PSPACE-completa. Ma questo nella pratica sembra limitare l'uso di CTL solo alla fase di specifica, lasciando spazio alla LTL per la verifica.
Curiosità: nella tua dimostrazione, oltre a provare che la tua logica ammette esattamente 25 modalità distinte, avevi generalizzato la relazione tra il numero di operatori e il conteggio totale delle modalità distinte ? Ovvero una risposta a domande come "Cosa succederebbe con sei operatori ? E con un N arbitrario (ovviamente finito) ?".
stiamo parlando della mia tesi di laurea di circa vent'anni fa.
secondo il mio professore doveva essere incentrata sulla concorrenza nei sistemi reattivi, ma, anche se quella parte è stata abbastanza approfondita, io in qualche modo l'ho un po' snobbata perché mi interessava di più la parte della logica temporale e perché avevo intravisto qualche cosa che io ero in grado di portare a termine, mi riferisco alle modalità nella logica Branching Time.
se hai modo di chiedere, o valutare tu stesso, ti posso dire che, a meno di dimostrazioni e altri collegamenti vari, il risultato principale è quello che ho indicato nel precedente post (quello che parla di esattamente 25 modalità distinte, tanto per intenderci). a parte il grafico che non sono capace di copiare e che quindi nella versione forum fa schifo, oltre che mancare delle frecce, gli operatori che qui ho chiamato A,B,C,D sono quelli descritti in qualche post precedente e si chiamerebbero "always, for-ever, sometimes, not-never". visto che la base per l'introduzione degli operatori branching viene da L. Lamport, mentre la struttura delle modalità prende spunto da A. Pnueli, sarebbe il caso di sapere se qualche risultato analogo è stato pubblicato nel frattempo oppure se c'è fermento dal punto di vista di queste ricerche o, ormai, non interessa più a nessuno.
francamente io ho abbandonato un po' per scelte lavorative, un po' perché non troppo "convinta" del mondo accademico (e le due cose non sono indipendenti!).
grazie per l'interessamento. a presto. ciao.
secondo il mio professore doveva essere incentrata sulla concorrenza nei sistemi reattivi, ma, anche se quella parte è stata abbastanza approfondita, io in qualche modo l'ho un po' snobbata perché mi interessava di più la parte della logica temporale e perché avevo intravisto qualche cosa che io ero in grado di portare a termine, mi riferisco alle modalità nella logica Branching Time.
se hai modo di chiedere, o valutare tu stesso, ti posso dire che, a meno di dimostrazioni e altri collegamenti vari, il risultato principale è quello che ho indicato nel precedente post (quello che parla di esattamente 25 modalità distinte, tanto per intenderci). a parte il grafico che non sono capace di copiare e che quindi nella versione forum fa schifo, oltre che mancare delle frecce, gli operatori che qui ho chiamato A,B,C,D sono quelli descritti in qualche post precedente e si chiamerebbero "always, for-ever, sometimes, not-never". visto che la base per l'introduzione degli operatori branching viene da L. Lamport, mentre la struttura delle modalità prende spunto da A. Pnueli, sarebbe il caso di sapere se qualche risultato analogo è stato pubblicato nel frattempo oppure se c'è fermento dal punto di vista di queste ricerche o, ormai, non interessa più a nessuno.
francamente io ho abbandonato un po' per scelte lavorative, un po' perché non troppo "convinta" del mondo accademico (e le due cose non sono indipendenti!).
grazie per l'interessamento. a presto. ciao.
Ciao Ada, grazie per avermi reindirizzato qui...
Come già accennato nell'altro thread, dalle mie parti si utilizzano CTL, CTL*, LTL per la specifica e verifica dei sistemi concorrenti in tempo reale (una volta si chiamavano "reattivi", più o meno quando la teoria della calcolabilità si chiamava "della ricorsione"), insieme ad un ricco arsenale di altre tecniche come le reti di Petri, i linguaggi formali (soprattutto algebrici: LOTOS, LARCH oltre all'immancabile "moderno" Z) di specifica e verifica, l'interpretazione astratta...
Dopo aver letto, ribadisco che il tuo sistema mi pare oltremodo interessante (e il nome di Pnueli è in copertina assieme a quello di Zohar Manna su uno dei più importanti manuali in materia). Che ne dici di preparare un PDF, magari da latex ?
Come già accennato nell'altro thread, dalle mie parti si utilizzano CTL, CTL*, LTL per la specifica e verifica dei sistemi concorrenti in tempo reale (una volta si chiamavano "reattivi", più o meno quando la teoria della calcolabilità si chiamava "della ricorsione"), insieme ad un ricco arsenale di altre tecniche come le reti di Petri, i linguaggi formali (soprattutto algebrici: LOTOS, LARCH oltre all'immancabile "moderno" Z) di specifica e verifica, l'interpretazione astratta...
Dopo aver letto, ribadisco che il tuo sistema mi pare oltremodo interessante (e il nome di Pnueli è in copertina assieme a quello di Zohar Manna su uno dei più importanti manuali in materia). Che ne dici di preparare un PDF, magari da latex ?
forse ho trovato un modo per inserire il contenuto della ricerca, anche se in maniera parziale... ho usato lettere anziché i soliti simboli, e non sono riuscita, per ora, a copiare le frecce... spero che si capisca qualcosa...
TEOREMA.
Esistono esattamente 25 modalità distinte nel sistema BT, di cui:
1 di grado 0 (*);
4 di grado 1 (A, B, C, D);
8 di grado 1 (AC, AD, BC, BD, CA, CB, DA, DB);
6 di grado 3 (ADA, ADB, ACB, DAC, DAD, DBC);
4 di grado 4 (ADAC, ADBC, DACB, DADB);
2 di grado 5 (ADACB, DADBC);
nessuna di grado maggiore di 5.
Lo schema generale è il seguente (le frecce indicano implicazioni):
A
......................... CA
................................................ ADA
.................. ACB
................................. ADACB......................... DA
B
................ AC............ ADB
............................................... DACB
CB
................................................ DADB
.................................. *
................ ADAC
............................................................... BC
................ ADBC
.................................. DAC.......... DB
................................................................. C
AD............................ DADBC
................................................ DBC
................. DAD
................................ BD
................................................................ D
TEOREMA.
Esistono esattamente 25 modalità distinte nel sistema BT, di cui:
1 di grado 0 (*);
4 di grado 1 (A, B, C, D);
8 di grado 1 (AC, AD, BC, BD, CA, CB, DA, DB);
6 di grado 3 (ADA, ADB, ACB, DAC, DAD, DBC);
4 di grado 4 (ADAC, ADBC, DACB, DADB);
2 di grado 5 (ADACB, DADBC);
nessuna di grado maggiore di 5.
Lo schema generale è il seguente (le frecce indicano implicazioni):
A
......................... CA
................................................ ADA
.................. ACB
................................. ADACB......................... DA
B
................ AC............ ADB
............................................... DACB
CB
................................................ DADB
.................................. *
................ ADAC
............................................................... BC
................ ADBC
.................................. DAC.......... DB
................................................................. C
AD............................ DADBC
................................................ DBC
................. DAD
................................ BD
................................................................ D
grazie ad entrambi. ho scaricato alcuni articoli del prof. Bonanno. effettivamente ho trovato molte analogie con la struttura di una parte della mia tesi. avrò comunque bisogno di un po' di tempo per rendermi conto di quanto ci sia di "comune" tra i nostri lavori, se gli assiomi di base sono analoghi e soprattutto se gli sviluppi e le strade aperte indicate portano a mete comuni. grazie ancora a Fioravante Patrone. quanto al suggerimento di PaoloC circa l'inserimento di un'immagine, devo dire che io non ho un sito internet... proverò creare un grafico su un file in più modalità sperando che si legga... ciao.
@adaBTTLS
scusa se insisto, ma perche' non dai un'occhiata qui?
http://www.econ.ucdavis.edu/faculty/bonanno/wpapers.htm
@PaoloC
sono d'accordo con te: sia la teoria del caos che i problemi relativi alla complessita' contengono aspetti interessanti, seri, innovativi, etc. Persino l'idea di "proprieta' emergente" non e' da buttare. Interessante anche la logica temporale
E' il mix che mi insospettisce e mi fa venire in mente quelli che si occupano di coaching, della miscion, del blablabla...
scusa se insisto, ma perche' non dai un'occhiata qui?
http://www.econ.ucdavis.edu/faculty/bonanno/wpapers.htm
@PaoloC
sono d'accordo con te: sia la teoria del caos che i problemi relativi alla complessita' contengono aspetti interessanti, seri, innovativi, etc. Persino l'idea di "proprieta' emergente" non e' da buttare. Interessante anche la logica temporale
E' il mix che mi insospettisce e mi fa venire in mente quelli che si occupano di coaching, della miscion, del blablabla...
"adaBTTLS":
... utilizzare la logica del tempo lineare significa considerare al futuro solo una possibilità, quella che si considera reale; al contrario la logica del tempo ramificato ha una rappresentazione ad albero, ogni cammino rappresenta una possibilità ed ogni nodo rappresenta un istante su più cammini ...
Mi sembra un peccato che queste tue ricerce siano rimaste nel cassetto. A semplice titolo di curiosità, la fisica quantistica rivela dei paradossi che per essere risolti avrebbero bisogno di concepire una realtà ramificata su più cammini ad un medesimo istante. Chissa ...
"adaBTTLS":
se volete sapere di più circa la "disposizione" delle 25 modalità distinte, dovete spiegarmi come fare per introdurre un grafico nel messaggio...
Immagino che si tratti di una immagine, allora dovrai caricare l'immagine su un sito internet, poi copi il collegamento (percorso con nomefile) e lo incolli sul messaggio che stai scrivendo, poi lo includi tra i tags e il gioco è fatto.
"Fioravante Patrone":
caro PaoloC, leggi pure, ci mancherebbe. Ma diffidare, diffidare! Tieni ben sveglio il senso critico.
Certamente, spesso anche io mi chiedo se mi sto trovando difronte ad inutili speculazioni, ma bisogna pur ammettere che la teoria del caos ha dato i suoi risultati, gli attratori ne sono un esempio. Riguardo la teoria della complessità, chiaro che non la possiamo elevare al rango di altre teorie, io penso che per ora sia una semplice proposta, tuttavia mi sembra sia l'unico approccio che abbiamo nel descrivere il comportamento emergente di un sistema.
tanto per dare un'idea della distinzione tra tempo lineare e tempo ramificato, partiamo dai due operatori base della logica modale: L (della necessità) ed M (della possibilità). non saprei come introdurre dei simboli, per cui continuo ad utilizzare L ed M anche per indicare operatori temporali. se A è una formula ben formata, LA significa "A vero ora ed in ciascuno degli istanti successivi", MA significa "A vero ora oppure vero in almeno uno degli istanti successivi". utilizzare la logica del tempo lineare significa considerare al futuro solo una possibilità, quella che si considera reale; al contrario la logica del tempo ramificato ha una rappresentazione ad albero, ogni cammino rappresenta una possibilità ed ogni nodo rappresenta un istante su più cammini (un solo cammino "al passato", nodo radice [presente] di un sottoalbero che rappresenta infiniti cammini "al futuro"). i "due" operatori diventano "quattro", a due a due duali:
- vero ora ed in ogni istante futuro di qualsiasi cammino;
- vero ora ed in ogni istante futuro di almeno un possibile cammino;
- vero ora oppure vero in almeno un istante futuro di qualsivoglia possibile cammino;
- vero ora oppure vero in almeno un istante futuro di almeno un possibile cammino.
nella mia tesi ho dimostrato che ci sono esattamente 25 modalità distinte nel sistema di logica del tempo ramificato che io ho chiamato "puramente temporale", mentre le modalità scendono a 5 se si considera il tempo lineare. ho studiato il sistema DX di Pnueli, che però non rispondeva alla mia idea appunto di "puramente temporale". l'idea di estensione ai quattro operatori l'ho presa da Lamport, come ho detto nel primo messaggio, anche se nell'articolo citato si estende solo uno dei due operatori (quello che ora ho chiamato M); io ho esteso in maniera perfettamente simmetrica l'altro operatore (L): a definirlo quindi non ci è voluto nulla... solo che il lavoro successivo è stato abbastanza impegnativo...
dimenticavo, una modalità è una parola (di un numero di lettere arbitrario, anche nullo, anche con ripetizione) sull'alfabeto dei "quattro" simboli che indicano gli operatori di base.
per ora mi sembra più che sufficiente, spero di non avervi annoiati oltre misura...
se volete sapere di più circa la "disposizione" delle 25 modalità distinte, dovete spiegarmi come fare per introdurre un grafico nel messaggio....
grazie dell'interessamento. ciao.
- vero ora ed in ogni istante futuro di qualsiasi cammino;
- vero ora ed in ogni istante futuro di almeno un possibile cammino;
- vero ora oppure vero in almeno un istante futuro di qualsivoglia possibile cammino;
- vero ora oppure vero in almeno un istante futuro di almeno un possibile cammino.
nella mia tesi ho dimostrato che ci sono esattamente 25 modalità distinte nel sistema di logica del tempo ramificato che io ho chiamato "puramente temporale", mentre le modalità scendono a 5 se si considera il tempo lineare. ho studiato il sistema DX di Pnueli, che però non rispondeva alla mia idea appunto di "puramente temporale". l'idea di estensione ai quattro operatori l'ho presa da Lamport, come ho detto nel primo messaggio, anche se nell'articolo citato si estende solo uno dei due operatori (quello che ora ho chiamato M); io ho esteso in maniera perfettamente simmetrica l'altro operatore (L): a definirlo quindi non ci è voluto nulla... solo che il lavoro successivo è stato abbastanza impegnativo...
dimenticavo, una modalità è una parola (di un numero di lettere arbitrario, anche nullo, anche con ripetizione) sull'alfabeto dei "quattro" simboli che indicano gli operatori di base.
per ora mi sembra più che sufficiente, spero di non avervi annoiati oltre misura...
se volete sapere di più circa la "disposizione" delle 25 modalità distinte, dovete spiegarmi come fare per introdurre un grafico nel messaggio....
grazie dell'interessamento. ciao.
caos?
complessita'?
logica temporale, cespugliosa o no?
mancano solo i fuzzy set e la teoria delle catastrofi, poi la compagnia di giro e' al completo
chissa' perche' i tromboni (tipo quelli che fanno master per i "vincenti") si riempiono spesso la bocca di questo novellame, innaffiato da un po' di brunello che brunello non e'
caro PaoloC, leggi pure, ci mancherebbe. Ma diffidare, diffidare! Tieni ben sveglio il senso critico.
cari saluti da un matematico reazionario
complessita'?
logica temporale, cespugliosa o no?
mancano solo i fuzzy set e la teoria delle catastrofi, poi la compagnia di giro e' al completo
chissa' perche' i tromboni (tipo quelli che fanno master per i "vincenti") si riempiono spesso la bocca di questo novellame, innaffiato da un po' di brunello che brunello non e'
caro PaoloC, leggi pure, ci mancherebbe. Ma diffidare, diffidare! Tieni ben sveglio il senso critico.
cari saluti da un matematico reazionario
É qualche tempo che sto cercando di approfondire (solo come lettura) la teoria del caos e la teoria della complessità.
Debbo dire che la Logica temporale Lineare (LTL) è citata spesso come base importante per la matematizzazione della teoria, soprattutto nella realizzazione di modelli descrittivi sull'evoluzioni dei sistemi complessi come i moti vorticosi nei fluidi, l'evoluzione del clima, l'evoluzione biologica e molecolare, nella realizzazione di algoritmi genetici... e via dicendo.
Penso che la logica tempo lineare sia funzionale anche all'evoluzione degli attratori strani http://it.youtube.com/watch?v=RYZ4N8D9aI0
La logica tempo ramificata invece mi è ignota, non so neppure cosa sia.
Debbo dire che la Logica temporale Lineare (LTL) è citata spesso come base importante per la matematizzazione della teoria, soprattutto nella realizzazione di modelli descrittivi sull'evoluzioni dei sistemi complessi come i moti vorticosi nei fluidi, l'evoluzione del clima, l'evoluzione biologica e molecolare, nella realizzazione di algoritmi genetici... e via dicendo.
Penso che la logica tempo lineare sia funzionale anche all'evoluzione degli attratori strani http://it.youtube.com/watch?v=RYZ4N8D9aI0
La logica tempo ramificata invece mi è ignota, non so neppure cosa sia.
mi sono persa una "a": ovviamente parlo di "sistemi reattivi", anche se di tale argomento si sono occupati tanti altri ed io solo marginalmente. scusate il refuso. ciao.
per il momento grazie. per ora aggiungo solo che, anche se l'argomento non riguardava strettamente l'intelligenza artificiale, era collegato con la concorrenza nei sistemi rettivi, quindi genericamente con l'informatica teorica. nei prossimi giorni, quando avrò un po' più di tempo, potrò essere più precisa nell'indicare l'oggetto della ricerca. ciao.
Sempre grazie a Google, con la query: temporal logic artificial intelligence si trovano delle pagine interessanti.
Tra cui, la presenza di questo corso alla Brandeis:
COSI 112: Temporal Logic in Artificial Intelligence http://www.cs.brandeis.edu/~cs112/cs112-2004/
che mi fa pensare si possa dare una risposta positiva a codino75
Anche se il programma del corso mi sembra molta TL e poca AI...
Menziono anche questo:
http://plato.stanford.edu/entries/logic-temporal/
(e' nella ben nota "Stanford Enciclopedia of Philosophy")
magari puo' interessare ad adaBTTLS
Tra cui, la presenza di questo corso alla Brandeis:
COSI 112: Temporal Logic in Artificial Intelligence http://www.cs.brandeis.edu/~cs112/cs112-2004/
che mi fa pensare si possa dare una risposta positiva a codino75
Anche se il programma del corso mi sembra molta TL e poca AI...
Menziono anche questo:
http://plato.stanford.edu/entries/logic-temporal/
(e' nella ben nota "Stanford Enciclopedia of Philosophy")
magari puo' interessare ad adaBTTLS
non so se ho capito bene il tema, ma forse c'entra con l'intelligenza artificiale?
Cercando:
temporal logic game theory
con Google vengono fuori un po' di cose.
Il che non è sorprendente.
Personalmente non mi occupo di questi aspetti, ma la breve bibliografia che trovi nella pagina (vecchiotta) di Baltag non mi è del tutto ignota.
Sul tema, un buon riferimento è Giacomo Bonanno, nostro "antico" emigrato a Davis. E puoi anche chiedere direttamente a lui, se ti pare in tema. Tra l'altro, un titolo come "A sound and complete temporal logic for belief revision" mi sembra un interessante mix
temporal logic game theory
con Google vengono fuori un po' di cose.
Il che non è sorprendente.
Personalmente non mi occupo di questi aspetti, ma la breve bibliografia che trovi nella pagina (vecchiotta) di Baltag non mi è del tutto ignota.
Sul tema, un buon riferimento è Giacomo Bonanno, nostro "antico" emigrato a Davis. E puoi anche chiedere direttamente a lui, se ti pare in tema. Tra l'altro, un titolo come "A sound and complete temporal logic for belief revision" mi sembra un interessante mix
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo