A Formal Interactive Verification Environment for the Plan Execution Interchange Language

The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal ex...

Full description

Autores:
Cadavid Rengifo, Hector Fabio
Rocha, Camilo
Muñoz, Cesar
Tipo de recurso:
Part of book
Fecha de publicación:
2012
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1838
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1838
Palabra clave:
Comprobación del modelo
Lógica Temporal Lineal
Proposición atómica
Lenguaje síncrono
Estructura Kripke
Model Check
Linear Temporal Logic
Atomic Proposition
Plan Execution
Kripke Structure
Rights
closedAccess
License
© Springer Nature Switzerland AG 2018