Un nuevo enfoque para invariantes no lineales para sistemas híbridos basado en el método de instancias citadas
Autores: He, Honghui; Wu, Jinzhao
Idioma: Inglés
Editor: MDPI
Año: 2020
Acceso abierto
Artículo científico
2020
Un nuevo enfoque para invariantes no lineales para sistemas híbridos basado en el método de instancias citadas
Categoría
Gestión y administración
Subcategoría
Gestión de la tecnología y la inovación
Palabras clave
Generación de invariantes
Sistemas híbridos
Relaciones de transición
Condiciones inductivas
Base de Gröbner
Método de Instancias Citadas
Licencia
CC BY-SA – Atribución – Compartir Igual
Consultas: 1
Citaciones: Sin citaciones
Al generar invariantes para sistemas híbridos, una fuente principal de intractabilidad es que las relaciones de transición son afirmaciones de primer orden sobre las variables del estado actual y las variables del siguiente estado, lo que duplica el número de variables del sistema e introduce muchas más variables libres. Cuantas más variables, menos tractabilidad y, por lo tanto, resolver las restricciones algebraicas sobre condiciones inductivas completas mediante una base de Gröbner integral es muy costoso. Para abordar este problema, este artículo presenta un nuevo método completo, llamado Método de Instancias Citadas (CIM), que puede eliminar las variables libres y resolver directamente las condiciones inductivas completas. Una instancia significa la verificación de una proposición después de instanciar variables libres a números. Un arreglo de reticulado es una noción clave en este artículo, que es esencialmente un conjunto finito de instancias. Verificar que una proposición se sostiene sobre un Arreglo de Reticulado es suficiente para probar que la proposición se sostiene en general; esta característica interesante nos inspira a presentar CIM. Por un lado, en lugar de calcular una base de Gröbner integral, CIM utiliza un Arreglo de Reticulado para generar las restricciones en paralelo. Por otro lado, podemos hacer un uso inteligente del paralelismo de CIM para comenzar con algunas ecuaciones de restricción que se pueden resolver fácilmente, con el fin de determinar algunos parámetros en un estado temprano. Estos parámetros resueltos benefician la solución del resto de las ecuaciones de restricción; este proceso es similar al efecto dominó. Por lo tanto, la tractabilidad de la resolución de restricciones del método propuesto es fuerte. Mostramos que algunos enfoques existentes son solo casos especiales de nuestro método. Además, resulta que CIM es más eficiente que los enfoques existentes en circunstancias paralelas. Se presentan algunos ejemplos para ilustrar la practicidad de nuestro método.
Descripción
Al generar invariantes para sistemas híbridos, una fuente principal de intractabilidad es que las relaciones de transición son afirmaciones de primer orden sobre las variables del estado actual y las variables del siguiente estado, lo que duplica el número de variables del sistema e introduce muchas más variables libres. Cuantas más variables, menos tractabilidad y, por lo tanto, resolver las restricciones algebraicas sobre condiciones inductivas completas mediante una base de Gröbner integral es muy costoso. Para abordar este problema, este artículo presenta un nuevo método completo, llamado Método de Instancias Citadas (CIM), que puede eliminar las variables libres y resolver directamente las condiciones inductivas completas. Una instancia significa la verificación de una proposición después de instanciar variables libres a números. Un arreglo de reticulado es una noción clave en este artículo, que es esencialmente un conjunto finito de instancias. Verificar que una proposición se sostiene sobre un Arreglo de Reticulado es suficiente para probar que la proposición se sostiene en general; esta característica interesante nos inspira a presentar CIM. Por un lado, en lugar de calcular una base de Gröbner integral, CIM utiliza un Arreglo de Reticulado para generar las restricciones en paralelo. Por otro lado, podemos hacer un uso inteligente del paralelismo de CIM para comenzar con algunas ecuaciones de restricción que se pueden resolver fácilmente, con el fin de determinar algunos parámetros en un estado temprano. Estos parámetros resueltos benefician la solución del resto de las ecuaciones de restricción; este proceso es similar al efecto dominó. Por lo tanto, la tractabilidad de la resolución de restricciones del método propuesto es fuerte. Mostramos que algunos enfoques existentes son solo casos especiales de nuestro método. Además, resulta que CIM es más eficiente que los enfoques existentes en circunstancias paralelas. Se presentan algunos ejemplos para ilustrar la practicidad de nuestro método.