En lógica matemática , la lógica monádica de segundo orden ( MSO ) es el fragmento de la lógica de segundo orden donde la cuantificación de segundo orden se limita a la cuantificación sobre conjuntos. [1] Es particularmente importante en la lógica de los gráficos , debido al teorema de Courcelle , que proporciona algoritmos para evaluar fórmulas monádicas de segundo orden sobre gráficos de ancho de árbol acotado .
La lógica de segundo orden permite la cuantificación sobre predicados . Sin embargo, MSO es el fragmento en el que la cuantificación de segundo orden se limita a predicados monádicos (predicados que tienen un solo argumento). Esto se describe a menudo como cuantificación sobre "conjuntos" porque los predicados monádicos son equivalentes en poder expresivo a conjuntos (el conjunto de elementos para los que el predicado es verdadero).
Complejidad computacional de la evaluación
La lógica monádica existencial de segundo orden (EMSO) es el fragmento de MSO en el que todos los cuantificadores sobre conjuntos deben ser cuantificadores existenciales , fuera de cualquier otra parte de la fórmula. Los cuantificadores de primer orden no están restringidos. Por analogía con el teorema de Fagin , según el cual la lógica existencial (no monádica) de segundo orden captura precisamente la complejidad descriptiva de la clase de complejidad NP , la clase de problemas que pueden expresarse en la lógica existencial monádica de segundo orden se ha denominado NP monádica. . La restricción a la lógica monádica hace posible probar separaciones en esta lógica que no han sido probadas para la lógica de segundo orden no monádica. Por ejemplo, en la lógica de los gráficos , probar si un gráfico está desconectado pertenece al NP monádico, ya que la prueba se puede representar mediante una fórmula que describe la existencia de un subconjunto adecuado de vértices sin bordes que los conecten con el resto del gráfico. ; sin embargo, el problema complementario, probar si un gráfico está conectado, no pertenece al NP monádico. [2] [3] La existencia de un par análogo de problemas complementarios, solo uno de los cuales tiene una fórmula existencial de segundo orden (sin la restricción de fórmulas monádicas) es equivalente a la desigualdad de NP y coNP , una cuestión abierta en computacional complejidad.
Por el contrario, cuando deseamos comprobar si una fórmula booleana MSO es satisfecha por un árbol finito de entrada , este problema puede resolverse en tiempo lineal en el árbol, traduciendo la fórmula booleana MSO a un árbol autómata [4] y evaluando el autómata en el árbol. Sin embargo, en términos de consulta, la complejidad de este proceso generalmente no es elemental . [5] Gracias al teorema de Courcelle , también podemos evaluar una fórmula booleana MSO en tiempo lineal en un gráfico de entrada si el ancho del árbol del gráfico está acotado por una constante.
Para fórmulas MSO que tienen variables libres , cuando los datos de entrada son un árbol o tienen un ancho de árbol limitado, existen algoritmos de enumeración eficientes para producir el conjunto de todas las soluciones, [6] asegurando que los datos de entrada se preprocesan en tiempo lineal y que cada solución luego se produce en un retardo lineal en el tamaño de cada solución, es decir, retardo constante en el caso común donde todas las variables libres de la consulta son variables de primer orden (es decir, no representan conjuntos). También existen algoritmos eficientes para contar el número de soluciones de la fórmula MSO en ese caso. [7]
Decidibilidad y complejidad de la satisfacibilidad
El problema de satisfacibilidad para la lógica monádica de segundo orden es indecidible en general porque esta lógica subsume la lógica de primer orden .
La teoría monádica de segundo orden del árbol binario completo infinito , llamada S2S, es decidible . [8] Como consecuencia de este resultado, las siguientes teorías son decidibles:
- La teoría monádica de segundo orden de los árboles.
- La teoría monádica de segundo orden de bajo sucesor (S1S).
- wS2S y wS1S, que restringen la cuantificación a subconjuntos finitos (lógica de segundo orden monádica débil). Tenga en cuenta que para los números binarios (representados por subconjuntos), la suma se puede definir incluso en wS1S.
Para cada una de estas teorías (S2S, S1S, wS2S, wS1S), la complejidad del problema de decisión no es elemental . [5] [9]
Uso de la satisfacebilidad de MSO en árboles en verificación
La lógica monádica de segundo orden de los árboles tiene aplicaciones en la verificación de software y, más ampliamente, en la verificación formal gracias a su decidibilidad y significativo poder expresivo. Se han implementado procedimientos de decisión para la satisfacción. [10] [11] [12] Estos procedimientos se utilizaron para probar las propiedades de los programas que manipulan estructuras de datos vinculadas, [13] como una forma de análisis de formas (análisis de programas) , así como para el razonamiento simbólico en la verificación de hardware. [14]
Referencias
- ^ Courcelle, Bruno ; Engelfriet, Joost (1 de enero de 2012). Estructura gráfica y lógica monádica de segundo orden: un enfoque teórico del lenguaje . Prensa de la Universidad de Cambridge. ISBN 978-0521898331. Consultado el 15 de septiembre de 2016 .
- ^ Fagin, Ronald (1975), "Monadic generalized spectra", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 21 : 89–96, doi : 10.1002 / malq.19750210112 , MR 0371623.
- ^ Fagin, R .; Stockmeyer, L .; Vardi, MY (1993), "On monadic NP vs. monadic co-NP", Actas de la Octava Conferencia Anual sobre Estructura en Teoría de la Complejidad , Instituto de Ingenieros Eléctricos y Electrónicos, doi : 10.1109 / sct.1993.336544.
- ^ Thatcher, JW; Wright, JB (1 de marzo de 1968). "Teoría generalizada de autómatas finitos con aplicación a un problema de decisión de lógica de segundo orden". Teoría de sistemas matemáticos . 2 (1): 57–81. doi : 10.1007 / BF01691346 . ISSN 1433-0490 .
- ^ a b Meyer, Albert R. (1975). Parikh, Rohit (ed.). "La teoría del sucesor de segundo orden monádico débil no es elemental-recursiva". Coloquio de lógica . Apuntes de clase en matemáticas. Springer Berlin Heidelberg: 132-154. doi : 10.1007 / bfb0064872 . ISBN 9783540374831.
- ^ Bagan, Guillaume (2006). Ésik, Zoltán (ed.). "Las consultas de MSO en estructuras de árbol descomponibles son computables con retardo lineal". Lógica informática . Apuntes de conferencias en Ciencias de la Computación. Springer Berlín Heidelberg. 4207 : 167-181. doi : 10.1007 / 11874683_11 . ISBN 9783540454595.
- ^ Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1 de junio de 1991). "Problemas fáciles para gráficos descomponibles en árboles". Revista de algoritmos . 12 (2): 308–340. doi : 10.1016 / 0196-6774 (91) 90006-K . ISSN 0196-6774 .
- ^ Rabin, Michael O. (1969). "Decidibilidad de las teorías de segundo orden y autómatas en árboles infinitos" . Transacciones de la American Mathematical Society . 141 : 1-35. doi : 10.2307 / 1995086 . ISSN 0002-9947 .
- ^ Stockmeyer, Larry; Meyer, Albert R. (1 de noviembre de 2002). "Cota inferior cosmológica en la complejidad del circuito de un pequeño problema de lógica" . Revista de la ACM . 49 (6): 753–784. doi : 10.1145 / 602220.602223 . ISSN 0004-5411 .
- ^ Henriksen, Jesper G .; Jensen, Jakob; Jørgensen, Michael; Klarlund, Nils; Paige, Robert; Rauhe, Theis; Sandholm, Anders (1995). Brinksma, E .; Cleaveland, WR; Larsen, KG; Margaria, T .; Steffen, B. (eds.). "Mona: lógica monádica de segundo orden en la práctica" . Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de conferencias en Ciencias de la Computación. Berlín, Heidelberg: Springer: 89-110. doi : 10.1007 / 3-540-60630-0_5 . ISBN 978-3-540-48509-4.
- ^ Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš (1 de abril de 2019). "Anticadenas anidadas para WS1S" . Acta Informatica . 56 (3): 205–228. doi : 10.1007 / s00236-018-0331-z . ISSN 1432-0525 .
- ^ Traytel, Dmitriy; Nipkow, Tobias (25 de septiembre de 2013). "Procedimientos de decisión verificados para MSO sobre palabras basadas en derivadas de expresiones regulares" . Avisos ACM SIGPLAN . 48 (9): 3–12. doi : 10.1145 / 2544174.2500612 . hdl : 20.500.11850 / 106053 . ISSN 0362-1340 .
- ^ Møller, Anders; Schwartzbach, Michael I. (1 de mayo de 2001). "El motor lógico de aserción de puntero" . Actas de la conferencia ACM SIGPLAN 2001 sobre diseño e implementación de lenguajes de programación . PLDI '01. Snowbird, Utah, EE. UU.: Asociación de Maquinaria de Computación: 221-231. doi : 10.1145 / 378795.378851 . ISBN 978-1-58113-414-8.
- ^ Cuenca, David; Klarlund, Nils (1 de noviembre de 1998). "Razonamiento simbólico basado en autómatas en la verificación de hardware" . Métodos formales en el diseño de sistemas . 13 (3): 255–288. doi : 10.1023 / A: 1008644009416 . ISSN 0925-9856 .