Modelització utilitzant Càlcul de Situacions

Índex

Descripció de l'àrea
URLs Relacionats
Treballs i papers realitzats sobre el tema

Descripció de l'àrea

A l'hora de modelitzar un problema, la millor manera de fer-ho és, sempre que siga possible, d'una manera formal. La lògica de primer ordre permet de formalitzar la majoria de problemes corrents que apareixen en el món de la informàtica en el que sí que s'utilitzen sovint les modelitzacions formals, per a posteriorment demostrar propietats o comprovar la correcció. Així es fa amb protocols de xarxes, sistemes operatius i software (encara que aquest últim és un món a banda).

El Càlcul de Situacions s'ha mostrat com un formalisme de primer ordre molt eficaç per a la modelització de sistemes dinàmics ja que el temps (les situacions) són intrínsiques al càlcul.

En el Càlcul de Situacions existix una situació inicial s0, a la qual és possible aplicar certes accions per arribar a altres situacions. La relació d'accesibilitat entre situacions es representa pel signe < (e.g. s1 < s2 signifia s2 és accessible des de s1). Aquells predicats que llur valor de veritat pot canviar arran la situació, s'anomenen fluents, i conseqüentment tenen un últim parametre temporal. Les accions tenen algunes precondicions, denotades per Poss. Si l'acció és possible, el resultat de fer-la en la situació s és una nova situació s'.

Actualment el centre més important que treballa en Càlcul de Situacions està liderat per Levesque, Reiter, Scherl i d'altres en Toronto (Canada). Un altre grup important es troba en la Escuela de Ingeniería de la Pontificia Universidad Católica de Chile, liderats per Javier Pinto i Leopoldo Bertossi, amb els quals vaig estar col.laborant directament durant l'estiu del 96 i amb els que continue projectes com "Formal Modelling of Cryptographic Protocols in Situation Calculus".

URL's sobre Modelitzció formal

(en construcció)

URL's sobre Càlcul de Situacions

(en construcció)

Investigadors Destacats o Autònoms:

(en construcció)
  • Escuela de Ingeniería Pontificia Universidad Católica de Chile, liderats per Javier Pinto i Leopoldo Bertossi.
  • Levesque, Reiter, Scherl i d'altres a Toronto (Canada)

    Escrits, treballs i esborranys que he fet sobre el tema

  • Protocolos Criptográficos en Cálculo de Situaciones
  • Viabilidad de un Modelo de Conocimiento Falible en Cálculo de Situaciones
  • Formal Modelling of Cryptographic Protocols in Situation Calculus

    Tornar a la plana major.
    © 1996-1997 José Hernández Orallo.