Análisis de complejidad de lógicas temporales

Análisis de complejidad de lógicas empo ales Complexi y analysis o empo al logics T abajo de Fin de G ado Cu so 2023–2024 Au o Se gio Ja ie He nando Ri e o Di ec o es Ismael Rod íguez Laguna Na alia López Ba quilla Doble g ado en Ingenie ía In o má ica y Ma emá icas Facul ad de In o má ica Uni e sidad Complu ense de Mad id Análisis de complejidad de lógicas empo ales Complexi y analysis o empo al logics T abajo de Fin de G ado de Doble G ado Ingenie ía In o má ica y Ma emá icas Au o Se gio Ja ie He nando Ri e o Di ec o es Ismael Rod íguez Laguna Na alia López Ba quilla Con oca o ia: Junio 2024 Doble g ado en Ingenie ía In o má ica y Ma emá icas Facul ad de In o má ica Uni e sidad Complu ense de Mad id 27 de Mayo de 2024 Ag adecimien os En p ime luga , quie o ag adece a mis u o es y di ec o es de abajo de in de g ado, Na alia López Ba quilla e Ismael Rod íguez Laguna, po b inda me apoyo, paciencia y expe iencia a lo la go de odo el p oceso. Además, les ag adezco habe me p opues o un ema an in e esan e y habe me p o is o de bibliog a ía pa a comenza el abajo. Ag adezco ambién a mi he mano Alejand o y a mis compañe os Jaime, Gonzalo y Amaia po sus consejos a la ho a de esc ibi y e ina mis a gumen os, así como su ayuda a la ho a de co egi e a as en el p opio abajo. Finalmen e, ex iendo mi g a i ud a odo el mundo que, de una o ma u o a, ha con ibuido en algún momen o del desa ollo de es e abajo. Resumen Análisis de complejidad de lógicas empo ales En es e T abajo de Fin de G ado (TFG) se lle a a cabo un es udio de la com- plejidad compu acional de la sa is acibilidad de lógicas empo ales. En pa icula , se analiza la complejidad de con a el núme o de in e p e aciones que hacen cie a una ó mula en LT L oLT L⋄, dos lógicas empo ales lineales. El obje i o p incipal de es e abajo es u iliza esul ados conocidos pa a la lógica LT L y deduci e- sul ados inno ado es sob e LT L⋄u ilizándolos. Además, es e documen o o ece un ace camien o a las lógicas empo ales y a las clases de complejidad, especialmen e a las clases de complejidad de con eo. En el desa ollo de es e abajo se dis inguen es ipos de in e p e aciones sob e los cuales el p oblema de la sa is acibilidad es de e minis a. Es as alo aciones em- po ales son las palab as pe iódicas, los k-á boles y los k-g a os. El análisis o mal de complejidad de con eo se ealiza conside ando cada uno de es os modelos de o ma independien e. Los esul ados ob enidos e lejan una simili ud en e la complejidad de con a modelos de palab as pe iódicas y k-g a os, debido a que es os modelos ienen un amaño simila . Po o o lado, se obse a una mayo complejidad en los k-á boles en elación a los o os dos ipos de modelos, ya que los k-á boles ienen una can idad de nodos exponencialmen e mayo . En esumen, es e abajo o ece una isión in eg al sob e la complejidad de con- eo en lógicas empo ales lineales, p opo cionando esul ados signi ica i os y es a- bleciendo una base pa a u u as in es igaciones en el análisis de LT L⋄. Palab as cla e Complejidad compu acional, Lógica empo al, LT L,LT L⋄, P oblemas de con eo, Model Coun ing, #P-comple i ud, #PSPACE-comple i ud. ii Abs ac Complexi y analysis o empo al logics In his Final Deg ee P ojec , we conduc an in-dep h analysis o compu a ional complexi y o sa is iabili y o empo al logics. In pa icula , we analyse he com- pu a ional complexi y o coun ing he numbe o in e p e a ions which sa is y an ins ance o LT L o LT L⋄, wo lineal- ime empo al logics. The main objec i e o his p ojec is he use o known esul s in LT L complexi y o deduce and p o e new esul s o LT L⋄. Addi ionally, his documen o e s an app oach o empo al logics and complexi y classes, in pa icula coun ing complexi y classes. In his p ojec , h ee ypes o models a e de ined: pe iodic wo ds, k- ees and k- g aphs. These models a e chosen because de e mining sa is iabili y in each o hese models is de e minis ic. This s udy o e s an independen analysis o he coun ing compu a ional complexi y o de e mining how many o each o hese models sa is y a ce ain o mula. The esul s ob ained show a simila i y be ween coun ing pe iodic wo d models and k-g aph models, mainly due o he simila size o hese models. Howe e , a signi ican di e ence is obse ed when analysing k- ees, exponen ially la ge ha he wo p io models. O e all, his p ojec o e s a gene al pe spec i e o e he coun ing complexi y in linea - ime empo al logic. I also helps p o ide signi ican esul s in LT L⋄analysis and ac s as a s epping s one o u u e esea ch in he opic. Keywo ds Compu a ional complexi y, Tempo al logic, LT L,LT L⋄, Coun ing p oblems, Model Coun ing, #P-comple eness, #PSPACE-comple eness ix 2Capí ulo 1. In oducción 1.2. Obje i os de la in es igación El obje i o de es e T abajo de Fin de G ado es analiza la complejidad de con a modelos que sa is acen una ó mula de LT L y u iliza esos esul ados pa a esol e p oblemas análogos empleando ó mulas de LT L⋄, una lógica empo al es ic amen- e con enida en LT L. O o obje i o es el ace camien o y amilia ización con lógicas empo ales y los azonamien os de complejidad, en pa icula los elacionados con la complejidad de con eo. 1.3. Plan de abajo Es e abajo se ha ealizado en dos ases: 1. In es igación: Du an e la ase de in es igación se es udió en p ime luga documen ación sob e clases de complejidad de con eo, comenzando po el ca- pí ulo 17 de A o a y Ba ak (2006), po ecomendación de los u o es. A aíz de eso, se buscó in o mación sob e azonamien os espacio- empo ales, con la in ención de o maliza el p oblema de de e mina el núme o de pasados p o- bables pa a si uaciones p esen es dadas. Una ez hecho es o, el obje i o e a analiza la complejidad del p oblema de la de e minación de pasados ac ibles en casos aplicados. T as una eunión con los u o es, se omó la decisión de gene aliza es e en oque y analiza la complejidad de lógicas empo ales. Así, se busca on a ículos elacionados con la complejidad de p oblemas de con eo en lógicas empo ales. Al habe encon ado, leído y comp endido el a ículo To ah y Zimme mann (2014), se decidió in es iga la complejidad de con a las soluciones a ó mulas en LT L⋄. 2. Desa ollo: Una ez se hubo conc e ado el obje i o de la in es igación, se u iliza on los esul ados ob enidos po o os au o es en complejidad de con eo de modelos en ó mulas de LT L pa a deduci y demos a nue os esul ados sob e la complejidad del p oblema de con a el núme o de modelos de ó mulas en LT L⋄. En pa icula , se dis inguie on es ipos de modelos dis in os en los que la sa is acibilidad es de e minis a y se ealizó un análisis de la complejidad de con a el núme o de cada uno de los ipos de modelos que sa is acen una ó mula en LT L⋄. 1.4. Es uc u a del abajo 3 1.4. Es uc u a del abajo El es o de es e abajo es á di idido en 5 capí ulos, siguiendo la es uc u a que se p esen a a con inuación: 1. El capí ulo 2 ac úa como p eámbulo, in oduciendo algunos concep os necesa- ios pa a comp ende la es uc u a y esul ados que se p esen an en el siguien e capí ulo. Se de inen clases de complejidad ele an es (así como una je a quía en e las mismas) y las dis in as lógicas sob e las cuales se in es iga á. 2. En el capí ulo 3 se encuen a el g ueso de es e T abajo de Fin de G ado. En es e se p esen a el abajo ealizado po el au o y los esul ados que se han demos ado, así como esul ados simila es de o os au o es. 3. El capí ulo 4 o ece una b e e ecopilación de los esul ados del capí ulo an e- io , un análisis de los mismos y posibilidades de abajo u u o. 4. Po úl imo, los capí ulos 5 y 6 es án o mados po aducciones al inglés de los capí ulos 1 y 4, espec i amen e. Cap´ ı ulo 2 Con ex o de la in es igación Pa a ealiza azonamien os lógicos sob e si uaciones ísicas, es necesa io un len- guaje lo su icien emen e exp esi o. Es e debe se capaz de o maliza adecuadamen e odos los enunciados que necesi amos. La lógica más u ilizada en ma emá icas es la lógica de p ime o den. Es a lógica es una combinación de lógica de p edicados y cuan i icado es. No obs an e, pa a ealiza azonamien os lógicos sob e conjun os sencillos se emplea una lógica conocida como lógica p oposicional. Es a es una lógica más sencilla que la lógica de p ime o den y que u iliza símbolos de p oposición que ep esen an ideas a ómicas y no incluye cuan i icado es. Una lógica p oposicional es á o mada po dos conjun os PyO, donde el p ime conjun o es llamado conjun o de símbolos de p oposición y el segundo se denomina conjun o de ope ado es. Se iene además que exis e una unción a :O → N, al que si a (o) = nse dice que oes un ope ado n-a io. Conside a emos que el conjun o Ocon iene los siguien es ope ado es: 1. ¬: ope ado una io de negación, es deci , in ie e el alo de e dad de la a i mación que lo sucede. 2. ∨: ope ado bina io que ep esen a el o lógico. 3. ∧: ope ado bina io que ep esen a el and lógico. 4. ⊥y⊤: ope ado es sin a gumen os que ep esen an la alsedad y la ce eza, espec i amen e. Dado un conjun o de símbolos de p oposición Py los ope ado es de O, se pueden de ini o malmen e las ó mulas del lenguaje LPsiguiendo las siguien es eglas de o mación: 1. ⊤y⊥ ∈ LP 2. ∀p∈ P,p∈LP 3. Si φ∈LP,¬φ∈LP 5 6Capí ulo 2. Con ex o de la in es igación 4. Si φ1, φ2∈LP, (φ1∗φ2)∈LP,donde ∗ ∈ {∧,∨} Los pa én esis en la ó mula an e io ac úan como complemen o sin ác ico a PyO. Habiendo de e minado la sin axis de la lógica p oposicional, su ge la idea na u al de de e mina si algo exp esado median e es as ó mulas puede se cie o o no. Es e p oblema es exac amen e SAT, el p oblema de sa is acibilidad booleana de una ó mula dada. Pa a lle a acabo la de e minación de e dad de una ó mula, es necesa io asigna un alo (cie o o also) a cada símbolo de p oposición de Py calcula el alo de e dad de las ó mulas usando la semán ica especí ica de cada ope ado . De inición 2.0.1. Una alo ación es una unción :P −→ {0,1}que hace co esponde a cada símbolo de p oposición un alo de e dad. Se deno a ⊥una ó mula que es siemp e alsa y ⊤una ó mula siemp e cie a. De inición 2.0.2. Dado un conjun o Pde símbolos de p oposición, φ∈LPuna ó mula y una alo ación :P −→ {0,1}, de inimos el alo de e dad de φcon y lo deno amos po φ po ecu sión es uc u al: 1. Sea φ∈ P,φ = (φ),⊥ = 0 y⊤ = 1 2. φ=¬φ′,φ =(0si φ′ = 1 1si φ′ = 0 3. φ=φ1∧φ2,φ = ∧(φ 1, φ 2), donde ∧(φ 1, φ 2) = (1si φ 1=φ 2= 1 0si φ 1= 0 oφ 2= 0 4. φ=φ1∨φ2, φ = ∨(φ 1, φ 2), donde ∨(φ 1, φ 2) = (1si φ 1= 1 oφ 2= 1 0si φ 1=φ 2= 0 La sa is acibilidad booleana de una ó mula φse cumple cuando exis e alguna alo ación al que φ = 1. El hecho de que sea una alo ación que sa is ace φse deno a po |=φy se dice que es modelo de φ. A pa i de la sa is acibilidad de una ó mula podemos de ini la sa is acibilidad de un conjun o de ó mulas Φ⊆LP, que se iene cuando una alo ación sa is ace odas las ó mulas con enidas en Φ. Es o ambién se deno a po |= Φ. Finalmen e, si cualquie alo ación al que |= Φ cumple que pa a una cie a ó mula φ, |=φ, decimos que φes consecuencia lógica de Φy lo deno amos po Φ|=φ. 2.1. La lógica LT L o linea - ime empo al logic Exis en ex ensiones de la lógica p oposicional que incluyen o os ope ado es, cuyo obje i o es p opo ciona una mayo exp esi idad. Pa a de ini exp esiones ela i as 2.1. La lógica LT L o linea - ime empo al logic 7 al iempo, podemos añadi al lenguaje de lógica p oposicional un nue o pa áme o, T. Es e pa áme o ep esen a el iempo median e un conjun o in ini o o almen e o denado. Es o quie e deci que, dados dos elemen os 1, 2∈ T , 1< 2implica que 1sucede an es que 2y que ∀ 1, 2∈ T se iene 1< 2, 1> 2o 1= 2, po lo que no hay ami icaciones en el iempo. Con es a noción en men e podemos de ini la lógica LT L (linea - ime empo al logic) como una upla de es elemen os (P, O,T), cuyos ope ado es son los de inidos an e io men e pa a la lógica p oposicional más los siguien es: 1. Ope ado un il (bina io): φ1Uφ2indica que exis e un pun o donde se cumple la p opiedad φ2y la p opiedad φ1se cumple siemp e po lo menos has a ese pun o. 2. Ope ado elease (bina io): φ1Rφ2indica que φ2es cie o has a el p ime momen o en el que φ1lo es. En caso de que es o no ocu a, φ2debe se cie o siemp e 3. Ope ado nex (una io): Xφque indica que, deno ando po el ins an e ac ual, la p oposición se cumple en el ins an e + 1. La lógica LT L es un subconjun o de la lógica de p ime o den que incluye es ic- amen e a la lógica p oposicional. En ella, no odos los ope ado es apo an exp esi i- dad, po que UyRson igualmen e exp esi os. De hecho, el ope ado Rpuede se ex- p esado en é minos del ope ado Umedian e la cons ucción φ1Rφ2=¬(¬φ1Uφ2). Al habe añadido es os es ope ado es se ob iene una lógica mucho más exp e- si a que la lógica p oposicional. A pa i de los ope ado es p oposicionales y los que acabamos de de ini se pueden es ablece ope ado es como los ope ado es una ios ⋄ (en algún momen o) o □(siemp e en el u u o). El ope ado ⋄es exp esable con el ope ado Umedian e la cons ucción ⋄φ=⊤Uφy el ope ado □es deducible a pa i del ope ado ⋄median e la cons ucción □φ=¬⋄¬φ. De la misma mane a, el ope ado ⋄se puede exp esa de o ma análoga en é minos de □median e la cons ucción ⋄φ=¬□¬φ. Las eglas de o mación sin ác icas de LT L son las siguien es: 1. ∀φ∈LP, φ ∈ LT L. 2. Si φ∈ LT L,&φ∈ LT L donde &∈ {X,⋄,□} 3. Si φ1, φ2∈ LT L, (φ1∗φ2)∈ LT L,donde ∗ ∈ {U,R} Con es os ope ado es en men e, se de ine la lógica LT L⋄, que añade únicamen e los ope ado es ⋄y□an e io men e de inidos a la lógica p oposicional usual. Es e ipo de cons ucciones que emplean subconjun os de LT L se án obje o de es udio más adelan e. La sin axis ope acional de LT L⋄es análoga a la de LT L eliminando las cons ucciones que emplean X,UyR. 8Capí ulo 2. Con ex o de la in es igación No obs an e, no es amos en condiciones de hace azonamien os en es a lógica, ya que solo disponemos de he amien as pa a o maliza exp esiones. Es deci , no enemos una semán ica. Pa a ello necesi amos in oduci el concep o de alo ación empo al o in e p e ación. De inición 2.1.1. Una alo ación empo al o in e p e ación es una unción π:T → 2|P| que asigna a cada ins an e en Tel conjun o de las p oposiciones a ómicas que son cie as en . Se iene po an o π( )|=φcuando la alo ación inducida po la e aluación de πen el ins an e cumple |=φ. La aplicación de πsob e cualquie exp esión en LT L se de ine po inducción es uc u al. Sea un ins an e de iempo cualquie a: 1. π( )|=⊥yπ( )|=⊤. 2. π( )|=ppa a p∈ P si p∈π( ). 3. π( )|=¬φsi π( )|=φ. 4. π( )|=φ1∧φ2si π( )|=φ1yπ( )|=φ2. 5. π( )|=φ1∨φ2si π( )|=φ1oπ( )|=φ2. 6. π( )|=Xφsi π( + 1) |=φ. 7. π( )|=φ1Uφ2si ∃ 1≥ al que π( 1)|=φ2y∀ 2∈[ , 1]se iene π( 2)|=φ1. 8. π( )|=φ1Rφ2(si ∀ 1≥ , π( 1)|=φ2yπ( 1)|=φ1 o∃ 2> , π( 2)|=φ1yπ( 2)|=φ2. 9. π( )|=⋄φsi ∃ 1> al que π( 1)|=φ. 10. π( )|=□φsi ∀ 1≥ se cumple π( 1)|=φ. De la misma mane a que hemos de inido la sin axis de LT L⋄como una es- icción de la de LT L, de inimos su semán ica como una es icción de la an e io que elimina las cláusulas 6, 7 y 8 de la an e io lis a. Median e una analogía con la sección an e io , decimos que una alo ación empo al es un modelo de un conjun o de ó mulas Φ, deno ado po π( )|= Φ, si pa a cada φ∈Φ,π( )|=φ. Si pa a cada alo ación π( ) al que π( )|= Φ se cumple π( )|=φpa a una cie a ó mula φ∈ LT L, decimos que φes consecuencia lógica de Φ, deno ado po Φ|=φ. Además, deno a emos a pa i de es e momen o π|=φsi y solo si ∀ , π( )|=φ. Habiendo de inido las semán icas de las es lógicas que nos in e esan (LP,LT L yLT L⋄), enemos eglas que pe mi en in e i si una alo ación es modelo o no de una ó mula. El obje i o de es e TFG es analiza la complejidad de una a ian e del p oblema (que se de ini á más adelan e) de sa is acibilidad bajo dis in as con- diciones. Pa a ello es necesa io de ini la noción de clase de complejidad, así como in oduci una se ie de clases que apa ece án más adelan e. 2.2. Clases de complejidad 9 2.2. Clases de complejidad En complejidad compu acional, se dice que una clase de complejidad es un con- jun o de p oblemas que son simila men e complejos. Es a simili ud se mide con su endimien o en algún pa áme o, habi ualmen e iempo de compu ación o espacio en memo ia. 2.2.1. La clase de complejidad P La clase de complejidad Pes á de inida de o ma explíci a po los lenguajes que la o man. De inimos un lenguaje o mal L⊆ {0,1}∗como un conjun o de palab as con enidas en {0,1}∗. A pa i de un lenguaje o mal se puede de ini el p oble- ma de decisión asociado a ese lenguaje Lde e minando si una palab a cualquie a w∈ {0,1}∗es á con enida en L. Decimos que es e p oblema es á en la clase de com- plejidad Psi y solo si exis e una máquina de Tu ing de e minis a que lo decida en un iempo meno que P(n), donde P(n)es un polinomio de o den ini o. Se dice que un p oblema con enido en es a clase es polinómico. El pa áme o nse co esponde con el amaño de la en ada p opo cionada a la máquina. Un ejemplo de un p oblema en Pes la búsqueda de un elemen o en una lis a de nelemen os, que, suponiendo que lee y compa a un elemen o iene un cos e en iempo cons an e meno o igual a una cie a cons an e c, consis e simplemen e en eco e la cin a de la máquina de Tu ing has a encon a lo. En caso de e mina la cin a y no habe encon ado el elemen o, sabemos que no es á, po lo que el p o- blema es decidible. En es e caso pa icula , el iempo a dado es meno o igual a c·n. Se conocen una g an can idad de p oblemas en la clase P, y se suele conside a que los p oblemas en es a clase son compu acionalmen e asequibles, ya que pa a alo es de nsu icien emen e g andes, cualquie p og ama con un iempo de ejecu- ción mayo que odo polinomio esul a imp ac icable. De la misma mane a, se dice que los p oblemas que se ejecu an en iempo polinómico son a ables o " ácilmen e compu ables". Es a hipó esis se denomina esis de Cobham, cuyos de alles pueden se consul ados en Cobham (1965). Además, Pes una clase azonable e in ui i a desde el pun o de is a de un p o- g amado , ya que cualquie sub u ina e icien e que un p og amado diseña se ejecu a en iempo lineal, cuad á ico o alguna combinación de unciones con un iempo de ejecución polinómico de exponen e bajo. En gene al, si esas sub u inas se llaman desde p og amas e icien es, ob enemos así composiciones a bi a ias de polinomios, cuyos cos es de inen la clase P. 2.2.2. La clase de complejidad NP Es a clase de complejidad se co esponde con la noción in ui i a de se e icien- emen e e i icable, es deci , exis e una máquina de Tu ing que de e mina si una solución puede se e i icada en iempo polinómico. Es o implica que la longi ud 10 Capí ulo 2. Con ex o de la in es igación de dichas soluciones no puede se demasiado g ande, como mucho polinómica en la longi ud de la en ada. A la ho a de de ini o malmen e es a noción de inimos la clase NP po los lenguajes L⊆ {0,1}∗pa a los cuales exis e un polinomio p:N→Ny una máquina de Tu ing M al que pa a cada x∈ {0,1}∗se iene x∈L⇐⇒ ∃u∈ {0,1}p(|x|) al que M(x, u) = 1 donde |x|es la longi ud de la palab a x. En es e caso se dice que ues un ce i icado pa a x espec o al lenguaje Ly la máquina M. Es e iden e que P ⊆NP, ya que si algo es compu able en iempo polinómico su esul ado se puede u iliza como e i icación. Se desconoce si P =NP, p oblema inmo alizado en los P oblemas del Milenio de la Clay Founda ion. 2.2.3. NP-comple i ud Decimos que un lenguaje L⊆ {0,1}∗es educible en iempo polinómico a o o lenguaje L′⊆ {0,1}∗, deno ado como L≤pL′, si exis e una unción compu able en iempo polinómico al que pa a cada x∈ {0,1}∗,x∈L⇐⇒ (x)∈L′. De es a mane a decimos que un p oblema L′es NP-du o si L≤pL′∀L∈NP. De la misma mane a, los p oblemas NP-comple os son aquellos que son NP-du os y es án con enidos en la p opia clase NP. Un caso de educciones pa icula men e in e esan e es el de las educciones pa si- mónicas, que p ese an el núme o de soluciones de ambos p oblemas. In o malmen e, ac úan como una biyección en e las soluciones de AyB. Fo malmen e, dada una ins ancia xdel p oblema A, una educción es pa simónica si el núme o de soluciones, o ce i icados, de xes igual al núme o de soluciones de (x), ins ancia del p oblema B. 2.2.4. Las clases PSPACE y NPSPACE De la misma mane a que se han de inido las clases de complejidad P y NP co- mo las clases cuyos p oblemas se pueden esol e y e i ica en iempo polinómico, espec i amen e, su ge la idea de de ini clases cuyos p oblemas se pueden esol e o e i ica empleando un espacio polinómico con el amaño de la en ada. La de inición o mal de ambas clases pasa po conside a las ya o ecidas an e- io men e con la excepción de cambia la idea de iempo o núme o de ope aciones po la de espacio en memo ia o amaño de la cin a de la máquina de Tu ing. De ini- mos así la clase PSPACE como el conjun o de los p oblemas de decisión que pueden 2.3. Los p oblemas de con eo y la clase de complejidad #P 11 se esuel os po una máquina de Tu ing de e minis a en espacio p(n)y iempo ili- mi ado, donde pes un polinomio en unción de n, el amaño de la en ada. Además, podemos de ini la clase NPSPACE como el conjun o análogo a PSPACE con una máquina de Tu ing no de e minis a. En e las clases p esen adas an e io men e se es ablecen las siguien es elaciones: P⊆NP ⊆PSPACE =NPSPACE La igualdad en e las dos úl imas clases iene dada po el eo ema de Sa i ch, consul able en Sa i ch (1970). 2.2.5. O as clases de complejidad También de ini emos las clases EXPTIME, EXPSPACE y 2EXPSPACE pa a en adas de amaño n. EXPTIME es la clase de complejidad que comp ende los p oblemas de decisión que pueden se esuel os po una máquina de Tu ing de e minis a u ilizando una can idad de iempo exponencial (en O(2p(n))). EXPSPACE, po o o lado, se e ie e a la clase de p oblemas de decisión esuel os po una máquina de Tu ing de e mi- nis a en una can idad de espacio en O(2p(n)). Finalmen e, 2EXPTIME deno a la clase de p oblemas de decisión que pueden se esuel os po una máquina de Tu ing de e minis a en un iempo en O(22p(n)). 2.3. Los p oblemas de con eo y la clase de comple- jidad #P Has a es e momen o se han mencionado únicamen e clases de p oblemas de de- cisión (cuya solución es bina ia y booleana) y las je a quías en e ellas. En muchas ocasiones, sin emba go, nos in e esa con a el núme o de ce i icados que esuel en el p oblema. Es o es undamen al en nume osas á eas, des acando en e ellas el cálcu- lo de p obabilidades. E ec i amen e, pa a pode de e mina la p obabilidad de un suceso es necesa io calcula el núme o de soluciones que iene un p oblema, po lo que el análisis compu acional del núme o de soluciones nos p opo ciona un análi- sis de la complejidad de es a a ea. De es a mane a, un p oblema de con eo ecibe la misma en ada que un p oblema de decisión, pe o su salida es un núme o na u- al que indica el núme o de posibles soluciones dis in as a esa de e minada ins ancia. Como ejemplo canónico de es a clase de p oblemas se emplea #SAT, la e sión de con eo del p oblema de sa is acibilidad booleana. Dada una ó mula p oposicional booleana φ, #SAT consis e en analiza el núme o de alo aciones dis in as que se pueden da a los símbolos de p oposición de φque sa is acen φ. Pa a analiza la complejidad de los p oblemas de con eo se de inen clases de com- plejidad p opias. La más empleada es la clase de complejidad #P, sha p-P o coun -P, 18 Capí ulo 3. Complejidad de dis in os modelos de lógica empo al Es udia emos en onces dis in as dependencias basadas en le as. De inición 3.0.1. Una le a es un conjun o de símbolos de p oposición que son cie os en un ins an e dado. Es as le as son exac amen e la e aluación π( )de una alo ación empo al πen un ins an e , pe o son denominadas le as pa a simpli ica y jus i ica la no ación en los es ipos de alo aciones empo ales que emplea emos en es e capí ulo: palab as pe iódicas, k-á boles y k-g a os. De nue o pa a simpli ica no ación y po analogía con la eo ía de g a os, es as le as ambién son conocidas como nodos en el es udio de k-á boles y k-g a os. En consecuencia, la acción de la aplicación πen el ins an e , de inida en 2.1.1, es asigna la le a que co esponde a dicho momen o y, con ello, de e mina qué p oposiciones a ómicas son cie as en ese ins an e. 3.1. Cadenas aco adas Hemos obse ado que no odas las alo aciones empo ales son igualmen e ú iles a la ho a de de e mina si son modelo o no de una de e minada ó mula. Po lo an o, nos in e esa conside a sólo in e p e aciones pa a las que podamos a i ma de o ma ini a y de e minis a si son o no modelo de una ó mula. Au o es en es e campo, en pa icula To ah y Zimme mann (2014), emplean es ipos de in e p e ación dis in a con es e p opósi o. Es as alo aciones empo ales de- ben ene su icien es egula idades como pa a pode de e mina de o ma p ecisa la e acidad de ó mulas y abajan con conjun os Tnume ables. Es os modelos son las palab as pe iódicas, los k-á boles y los k-g a os. Como b e e eco da o io, deci- mos que una in e p e ación πes modelo de una ó mula φcuando se iene π( )|=φ ∀ ∈ T . Po ejemplo, pa a la ó mula φ=□p(siemp e se cumple p) y T=N, las in e - p e aciones π1( ) = {p}yπ2( ) = {p, q} ∀ ∈ T son dos modelos de φ, mien as que la in e p e ación π3(1) = {p}, con π3( ) = {q} ∀ ∈ T ; = 1 no es modelo, ya que ∃ 0= 2 al que π( 0)|=φ. Cabe des aca que los ipos de in e p e ación que se mencionan más adelan e, los que se analizan en To ah y Zimme mann (2014), no son las únicas in e p e aciones que dan luga a modelos. En el a ículo Sis la y Cla ke (1985), p ime ace camien o al análisis de complejidad compu acional de lógicas empo ales, se emplean única- men e in e p e aciones abs ac as simila es a las palab as pe iódicas. Sin emba go, es e abajo es udia á es ipos de in e p e aciones de cadenas aco adas, po con- side a los más gene ales y di e sos. 3.1. Cadenas aco adas 19 3.1.1. Valo aciones empo ales basadas en palab as pe iódi- cas En la de inición 3.0.1 se ha de inido lo que es una le a, un conjun o de p oposi- ciones a ómicas cie as en un ins an e conc e o. Decimos en onces que una palab a de amaño kes un conjun o o denado de le as o mado po dos secuencias de le as uy o madas, a su ez, po secuencias cualesquie a de le as al que el núme o de le as o al sume k. Es deci , ales que |u|+| |=k, donde kes una cie a co a dada de an emano. Además, la secuencia se epi e a bi a iamen e. Decimos que ues el p e ijo y el pe iodo de la palab a u ( ∗), donde el as e isco indica que se puede epe i una can idad a bi a ia de eces (incluso ninguna), ep esen ando odas ellas la misma alo ación empo al. Es e signi icado del as e isco es exac amen e el usado habi ualmen e en la de inición de exp esiones egula es. Pa a ab e ia , deno a emos la palab a u ( ∗)de inida po las dos secuencias uy esc ibiendo u . Cada le a en la secuencia ep esen a una alo ación empo al en un ins an e de iempo y la ansición de una le a a o a se p oduce en cada ins an e, de ahí que necesi emos que el conjun o Tsea nume able pa a es e ipo de modelos. Como ejemplo de in e p e aciones basadas en palab as pe iódicas se mues an alo aciones empo ales aplicadas a la ó mula φ=□(p∨(q−→ X )). En la igu a 3.1 se obse a un modelo de longi ud 3, en la igu a 3.2 uno de longi ud 2 y en la igu a 3.3 una in e p e ación que no es modelo de φ. Figu a 3.1: Modelo de longi ud 3 Figu a 3.2: Modelo de longi ud 2 Figu a 3.3: In e p e ación empo al no modelo de φ 20 Capí ulo 3. Complejidad de dis in os modelos de lógica empo al 3.1.2. Valo aciones empo ales basadas en k-á boles Los dos siguien es ipos de in e p e ación es án menos basados en los lenguajes egula es y más en la eo ía de g a os. El p ime ipo de alo aciones empo ales es á basado en la noción de á bol di igido que se emplea habi ualmen e en eo ía de g a os. De es a mane a, las alo aciones en cada ins an e son llamadas nodos. Una alo ación empo al basada en un k-á bol es una in e p e ación cuyo com- po amien o se puede modeliza median e un g a o simila a un á bol di igido de al u a k, donde el es ado inicial (la alo ación en el p ime ins an e de iempo) es el nodo aíz y cuya anchu a po núme o de hijos es una cons an e cde e minada. Es as in e p e aciones no son exac amen e á boles, ya que además, de cada nodo hoja, pa e una a is a hacia algún nodo en la misma ama. De es a mane a, cada ama es una palab a pe iódica. Cada á bol de ine más de una in e p e ación π, ya que la le a co espondien e al ins an e + 1 co esponde a uno cualquie a de los hijos de la le a en el ins an e , sal o que es a sea una hoja (en cuyo caso la le a siguien e es de e minis a). De hecho, in ini as alo aciones empo ales dis in as pueden ene un mismo k- á bol asociado. Decimos que un k-á bol Aes modelo de una ó mula cuando odas las in e p e aciones cuyo k-á bol asociado es un subg a o de Ason modelo de dicha ó mula. El p oblema que nos in e esa en es e caso es con a el núme o de k-á boles di e en es que son modelo de una cie a ó mula. A con inuación se mues a en la igu a 3.4 un 2-á bol modelo de la ó mula φ=□(p∨(q−→ X )). Figu a 3.4: Modelo de 2-á bol de φ 3.1.3. Valo aciones empo ales basadas en k-g a os El úl imo ipo de alo aciones empo ales que es e abajo es udia á son las a- lo aciones basadas en k-g a os. Una alo ación empo al basada en un k-g a o es una in e p e ación cuyo com- po amien o se puede modeliza como un sis ema de ansiciones di igidas de k es ados, un g a o di igido donde cada es ado es alcanzable desde el inicial, e i ando así es ados inalcanzables y donde cada es ado puede ene a ias a is as salien es, 3.2. Model Coun ing 21 incluyendo au oa is as. Ocu e en es os modelos un enómeno simila al que se ob- se a en los k-á boles, ya que cada ansición en un nodo con a ias a is as salien es da luga a ese núme o de in e p e aciones dis in as. De nue o, nos in e esa á con a los k-g a os en los cuales odas las in e p e aciones son modelo de la ó mula que nos in e ese. En la igu a 3.5 se mues a un ejemplo de 4-g a o modelo de la ó mula LT L □(p∨(q−→ X )) que se mos ó an e io men e. Figu a 3.5: Modelo de 4-g a o de φ 3.2. Model Coun ing El p oblema que nos in e esa, a di e encia del en oque de decisión, más ecuen e y p eocupado po la exis encia de una única alo ación empo al que sea modelo de una ó mula, es con a el núme o de palab as pe iódicas, k-á boles o k-g a os que sa is acen una de e minada ó mula. Es e p oblema es equi alen e, en el caso gene al, a la búsqueda de in e p e a- ciones que son modelo de una ó mula, indecidible en muchos casos. P ecisamen e po es o se han de inido los modelos an e io es, di e enciando casos más o menos complicados. A lo la go de es a sección, las demos aciones sob e la complejidad de LT L p esen adas se pueden consul a en To ah y Zimme mann (2014). Se mues an algunas po su u ilidad pa a desa olla a gumen os p opios y o as po p opo ciona un con ex o comple o. Todas las demos aciones que hacen e e encia a LT L⋄son o iginales de es e abajo. 3.2.1. Model coun ing pa a modelos de palab as pe iódicas Habiendo de inido el p oblema que nos in e esa analiza , model coun ing, pa i- cula iza emos es e pa a con a las palab as pe iódicas de longi ud kque son modelo de una cie a ó mula en una lógica empo al. 22 Capí ulo 3. Complejidad de dis in os modelos de lógica empo al Comenza emos analizando el caso en el que kes un núme o dado en una io, don- de la ep esen ación de k oma exac amen e ese núme o de símbolos en la máquina de Tu ing. Es o con as a con el caso en el que kes á codi icado en bina io. Aquí, la ep esen ación de ken la cin a de la máquina de Tu ing emplea log2(k)símbolos. Fo malmen e co esponde con el p oblema: Dadas una ó mula de LT L φy una co a (esc i a en una io), ¿cuan as palab as pe iódicas de longi ud kmodelan φ? Teo ema 3.2.1. Model coun ing pa a cadenas pe iódicas aco adas con k una io pe enece a #P. Demos ación. Pa a e que es á en #P de inimos una máquina de Tu ing no de- e minis a Mde la siguien e mane a. La máquina adi ina un p e ijo uy un pe iodo de una palab a pe iódica, con |u |=ky comp ueba de o ma de e minis a en iempo polinómico si u modela φ. Po lo an o, cada ejecución de ine únicamen e una palab a y encon a odos los modelos se puede ealiza con ando las ejecuciones en las que Macep a. Tenemos además que es e p oblema es una gene alización de #SAT, ya que si ijamos k= 1 y una ó mula φ∈LPob enemos un caso pa icula de Model coun- ing pa a LT L yLT L⋄que se co esponde exac amen e con #SAT. Como #SAT es un p oblema #P-du o, cualquie gene alización del mismo lo es ambién. Dado que la ep esen ación en una io de 1es idén ica a su ep esen ación en bina io, es e esul ado se iene en ambos casos. Co ola io 3.2.1.1. Model coun ing pa a cadenas pe iódicas aco adas con k una io es #P-comple o. Si conside amos que la co a kes á esc i a en bina io, el p oblema cambia. Es a- íamos con es ando en onces al p oblema análogo: Dadas una ó mula de LT L φy una co a (esc i a en bina io), ¿cuán as palab as pe iódicas de longi ud kmodelan φ? Es e p oblema es #PSPACE-comple o. Pa a e lo comenza emos demos ando que es á en #PSPACE. Teo ema 3.2.2. Model coun ing pa a cadenas pe iódicas aco adas con kbina io pe enece a #PSPACE. Demos ación. No podemos simplemen e adi ina una palab a de longi ud kpo que es á codi icado en bina io (y el amaño de esa palab a es exponencial espec o al amaño de la en ada). Cons uimos en onces nues a máquina de Tu ing que adi ina una palab a e- p esen ada po u adi inando u$ , donde $ es un símbolo que indica el comienzo del pe iodo. De es a mane a, la palab a u$ se puede esc ibi como w(0)...w(i− 1)$w(i)...w(k−1), donde w(i)indica la le a i-ésima de la palab a u . El símbolo 3.2. Model Coun ing 23 $ es ú il únicamen e pa a deno a el comienzo del pe iodo. Pa a cumpli con los e- quisi os de espacio, la máquina Msolo almacena el símbolo w(j)pa a cada ins an e de iempo j∈ T , desca a símbolos adi inados an e io men e y lle a un con ado pa a adi ina exac amen e ksímbolos. Pa a e i ica que u |=φ,Mc ea pa a cada jen el ango 0≤j < k un conjun o Cjde sub ó mulas de φcon la in ención de que Cjcon enga exac amen e las sub ó mulas que se sa is acen en la posición jde u . De nue o, no podemos almacena odos los conjun os, así que se almacenan es conjun os: Cj,Cj+1 y Ck−1. El úl imo es adi inado po My los conjun os j < k −1se de e minan de o ma uní oca po las eglas siguien es: 1. La pe enencia a Cjde p oposiciones a ómicas es de e minado po w(j), po - que es e es una le a. 2. Las conjunciones, disyunciones y negaciones se comp ueban localmen e. Po ejemplo, ¬p∈Cjsii p /∈Cj. 3. Las ó mulas Xse p opagan hacia a ás usando la equi alencia: Xφ∈Cjsii φ∈Cj+1. 4. Las ó mulas que con ienen Uu ilizan la equi alencia: φ0Uφ1∈Cjsi y solo si se da φ1∈Cjo se da φ0∈Cjyφ0Uφ1∈Cj+1. 5. El es o de ope ado es se pueden eesc ibi en é minos de los an e io es (in- cluyendo R). Una ez Mha adi inado el pe iodo al comple o, comp ueba que el conjun o Ck−1 es co ec o. Es o ocu e si se e i ican los equisi os: 1. Pa a cada sub ó mula Xφse cumple Xφ∈Ck−1si y solo si φ∈Ci. 2. Pa a cada sub ó mula φ0Uφ1se cumple φ0Uφ1∈Ck−1si y solo si φ1∈Ck−1 oφ0∈Ck−1yφ0Uφ1∈Ci. Además, es necesa io que si φ0Uφ0∈Cjpa a algún jen e iyk, se enga ambién φ1∈Cj′pa a un j′en el mismo ango. Es a condición se comp ueba mien as se calculan los Cj. Po inducción es uc u al sob e la cons ucción de las ó mulas en LT L se iene que ψ∈Cjsi y solo si w(j)w(j+ 1)...w(k−1) ∗|=ψ, donde ψes cualquie sub ó mula de φ. Po ello, la palab a deseada es un modelo de φsi y solo si φ∈C0. Es o quie e deci que Macep a en es e caso. Pa a e mina de p oba la #PSPACE comple i ud, es necesa io e la #PSPACE- du eza del p oblema. El modelo gene al de las demos aciones de du eza del análisis de complejidad de model coun ing pa a modelos de palab as pe iódicas se basa en la cons ucción de una ó mula φ∈ LT L que modeliza el compo amien o de una cie a máquina de Tu ing no de e minis a Mcon alguna es icción en iempo y espacio en una en ada 24 Capí ulo 3. Complejidad de dis in os modelos de lógica empo al w. Dicha ó mula φcodi ica las ejecuciones posibles en las que Macep a, po lo que la deno a emos φw M. La di icul ad de es e p ocedimien o eside en cons ui es a ó mula de al mane a que el núme o de ejecuciones en las que Macep a sea igual al núme o de modelos de φw Mpa a cie o k, co a de la palab a pe iódica. Elegimos k de al mane a que una ejecución wde longi ud maximal se pueda codi ica en k−1 símbolos y de inimos φw Mde al mane a que solo con enga modelos cuyo pe iodo enga longi ud uno, es deci , que el p e ijo enga k−1le as y el pe iodo solamen e una. En caso de que una palab a que es modelo enga longi ud meno de k, bas a con epe i la úl ima le a has a llega a la longi ud deseada y conside a esas le as añadidas como pa e del p e ijo. Teo ema 3.2.3. Model coun ing con cadenas pe iódicas aco adas con kbina io es #PSPACE-du o. Demos ación. Sea M= (Q, q , QF,P, δ)una máquina de Tu ing no de e minis a de una cin a, donde Qes el espacio de es ados, q el es ado inicial, Q es el conjun o de es ados en los que Macep a, Pes el al abe o y δes la unción de ansición. M echaza cuando el es ado inal no es de acep ación. Sea Maco ada en espacio po un polinomio p(n),w=w0...wn−1una en ada de My o o polinomio p′(n) (que solo depende de M) al que M e mina en un núme o 2p′(n)pasos, el máximo núme o de con igu aciones dis in as de la máquina si enemos ese espacio, donde n es la longi ud de la en ada. Es a máquina mues a el compo amien o de cualquie lenguaje en #PSPACE, de o ma simila a la educción de cualquie p oblema en NP a Ci cui -SAT ealiza- da en el eo ema de Cook-Le in. El siguien e paso en la demos ación es la cons ucción de la ó mula φw My una co a k ep esen ada en amaño polinómico espec o a n al que el núme o de eje- cuciones en las que Macep a es el mismo que el núme o de palab as pe iódicas de longi ud kque modelan φw M. Una ejecución de Msob e wse codi ica po una secuencia ini a de id’s idi, donde cada id es una desc ipción del es ado de Men el ins an e i, incluyendo el con enido de la cin a, el es ado de la máquina y la cabece a. Pa a ello se emplean lcp oposi- ciones a ómicas ( ep esen ando los alo es de bi de cada id). Po lo an o, hay 2lc con igu aciones dis in as de la máquina. Es a sucesión se al e na con con igu aciones ci, que es án o madas po un símbolo único que indica si dos ids consecu i os son consis en es con la unción de ansición δde Mseguida po una epe ición de un símbolo es igo: $id0#c0$id1#c1... $id2lc #c2lc (⊥)ω pa a un cie o lc(que se de ini á más adelan e). El pe iodo de la palab a es de la o ma (⊥)lpa a algún l > 0. De inimos k al que las ejecuciones de longi ud maxi- mal de Men wpueden se codi icadas en el p e ijo. Los símbolos cison únicos pa a cada i, lo cual hace que cada una de las 2lccon igu aciones que son codi icadas sean 3.2. Model Coun ing 25 di e en es ( epi iendo la úl ima con igu ación si es necesa io has a alcanza el núme- o deseado de con igu aciones). Como la máquina se de iene po de inición as ese núme o de pasos, el pe iodo solo puede ene longi ud 1. Es o asegu a una elación 1:1 en e k-palab as y ejecuciones en las que Macep a. Sea l =p(n)el amaño maximal de la con igu ación de Men w. Pa a los ids se usa un con ado bina io con lc=p′(n)bi s. Las p oposiciones en Q∪Pse usan pa a codi ica las con igu aciones de Mcodi icando el con enido de la cin a, el es ado de la máquina y la posición de cabece a. Es as p oposiciones ep esen an los alo es de bi de cada id. Los símbolos $y#se usan como sepa ado es y el símbolo ⊥es un símbolo sin signi icado pa a ep esen a el pe iodo del modelo. La dis ancia en e símbolos sepa ado es es d=l +3. Es amos en condiciones de de ini φw Mcomo la conjunción de las siguien es ó mulas: 1. Id codi ica los ids de las con igu aciones. Emplea la ó mula Inc(b1, ...., blc, d) que a i ma que el núme o codi icado po los bi s de bdespués de dpasos se ob iene inc emen ando el núme o codi icado en la posición ac ual. 2. Ini a i ma que la ejecución de Mcomienza con la con igu ación inicial. 3. Accep a i ma que la ejecución alcanza una con igu ación donde Macep a. 4. Loop de ine el pe iodo del modelo, solo puede con ene ⊥. 5. Repea a i ma que la codi icación de un es ado acep ado se epi e has a que se alcance el id maximal. 6. Con ig decla a la consis encia de dos con igu aciones sucesi as con la ela- ción de ansición de M. Aquí, usamos dope ado es Xpa a elaciona la codi icación de las dos con igu aciones. La demos ación de que odas las p opiedades an e io es se pueden exp esa con ó - mulas de amaño polinómico y la aducción de cada ins ucción de Ma exp esiones en LT L se puede e en To ah y Zimme mann (2014). Además, se necesi a que cada ó mula especi ique una se ie de de alles: las p oposiciones a ómicas que codi ican los ids no pueden apa ece en las con igu aciones y ice e sa; los sepa ado es ($ y #) no pueden ene o os signi icados y apa ecen únicamen e 2p′(n) eces cada d posiciones; y las codi icaciones de las con igu aciones se ep esen an con conjun os únicos de le as de Pcon la excepción del conjun o de la cabece a, que con iene un símbolo de Q. Finalmen e, se p ueba que la ó mula iene las p opiedades deseadas: pa a k= 2lc∗(l + 3) + 1 (es e núme o su ge de las 2lcsecuencias de id y con igu ación p e- cedidas po un $, donde la dis ancia en e un $ y el siguien e $ es l + 3 y el úl imo símbolo añadido se debe al símbolo ⊥que ep esen a el pe iodo), cada ejecución de Men una en ada wdonde Macep a co esponde con exac amen e una palab a que modela φw Mque codi ica esa ejecución en su p e ijo. 26 Capí ulo 3. Complejidad de dis in os modelos de lógica empo al Po lo an o, se cumple esa equi alencia en e ejecuciones y modelos. La ó mula φw Mse puede ob ene en iempo polinómico en |w|+|M|, y kes exponencial en |w|, con lo que puede se codi icado en bina io con un núme o polinómico de bi s. En base a los dos eo emas an e io es, se iene el siguien e esul ado: Co ola io 3.2.3.1. El siguien e p oblema es #PSPACE-comple o: Dado una ó - mula LT L φy una co a kcodi icada en bina io, ¿cuán os modelos de palab as pe iódicas de longi ud k iene φ? Una ez hemos p obado el esul ado pa a la lógica LT L, su ge la p egun a de conside a el p oblema pa a la o a lógica empo al que se ha plan eado: LT L⋄. La e sión de decisión de model coun ing en palab as pe iódicas pa a LT L⋄es NP-comple a como esul ado de un eo ema de modelos pequeños, como se e en Schnoebelen (2002). Es e a i ma que, en caso de exis i algun modelo pa a la ó mula φ, exis e uno de amaño en O(|φ|). Si conside amos el p oblema de con eo asociado la si uación es di e en e. En e ec o, debemos conside a cualquie modelo de amaño k, no solo los de meno amaño. Teo ema 3.2.4. El siguien e p oblema es #P-comple o: Dada una ó mula LT L⋄φ y una co a kcodi icada de o ma una ia, ¿cuán os modelos de palab as pe iódicas de longi ud k iene φ? Hemos obse ado que LT L⋄es un subconjun o de LT L y que la lógica p opo- sicional usual es á con enida en ella. Al habe esuel o es e p oblema pa a ambas lógicas y habe se demos ado que es #P-comple o, sabemos que se cumple es e eo- ema, ya que al gene aliza #SAT se a a de un p oblema #P-du o y al se una pa icula ización del p oblema análogo en LT L es #P-comple o. Es e esul ado es poco ele an e compa ado con los que se ienen cuando k es á codi icado en bina io, dado que usualmen e se suele exp esa la en ada en ba- se compu acional. Aquí el esul ado es menos i ial, ya que model coun ing pa a LT L es #PSPACE-comple o y no podemos sabe con ce idumb e la di icul ad del p oblema po aco ación. Sabemos que LT L⋄es á en #PSPACE po se una pa i- cula ización de LT L, pe o se o ece una demos ación de es e hecho como mues a de cómo adap a demos aciones de LT L aLT L⋄. Teo ema 3.2.5. El siguien e p oblema es á en #PSPACE: Dada una ó mula LT L⋄φ y una co a kcodi icada en bina io, ¿cuán os modelos de palab as pe iódicas de lon- gi ud k iene φ? Demos ación. Es a demos ación a a p ocede de o ma muy simila al eo ema 3.2.2. El esquema de la demos ación consis e en adi ina una palab a u le a a le- a (deno amos la le a adi inada en un ins an e jcomo w(j)) y e i ica en iempo polinómico que es a palab a es un modelo pa a la ó mula φ. 3.2. Model Coun ing 27 La lógica LT L⋄puede exp esa se con la lógica p oposicional unida al ope ado □, cuyo signi icado eco damos. Se iene que □φsi y solo si φse cumple siemp e. Pa a e i ica que u |=φ, la máquina debe c ea al comienzo un conjun o C0que con iene odas las sub ó mulas de φque se sa is acen con la asignación inicial de alo es en la p ime a le a de la palab a. Pa a una ó mula conc e a, de e mina el núme o de sub ó mulas con enidas en ella es lineal y el espacio que equie e acumula las es cuad á ico. Con cada ins an e ise adi ina la le a i-ésima de la in e p e ación u y se ac ualiza el conjun o Ci, que es el que se á almacenado, siguiendo el siguien e esquema: 1. La pe enencia a Cide p oposiciones a ómicas es de e minado po w(i). 2. Las conjunciones, disyunciones y negaciones se comp ueban localmen e. Po ejemplo, ¬p∈Cjsi y solo si p /∈Cj. 3. Las ó mulas de la o ma □ψapa ecen en Cisi ψ∈Ciy□ψ∈Ci−1. Pa a cada ins an e ise almacenan únicamen e dos conjun os, Ci−1yCiy se iene u |=φsi φ∈Ck, donde kes el amaño de la palab a, es deci , Ckes el úl imo conjun o. Po an o se iene que la ó mula se e i ica con un espacio asin ó icamen e cons an e y, po an o, el p oblema es á en #PSPACE. Pa ece en onces que el p oblema es á en e #P y #PSPACE. Nos gus a ía sabe si es #P-comple o o si, po o a pa e, no es á en #P, pe o es a no es una dis inción i ial. Pa a discu i lo ol e emos a la de inición de la clase #P, en la sección 2.3. Ob- se amos que un p oblema de con eo pe enece a es a clase si exis e una máquina de Tu ing no de e minis a M al que el núme o de caminos en los que Macep a es igual a la solución del p oblema de con eo. Si enemos que una k-palab a es modelo de una cie a ó mula φpe o Mno puede e i ica la en iempo polinómico, pa ece- ía lógico que no es u ie a con enido en #P. Sin emba go, es o no es del odo co ec o, ya que es posible que exis a o a má- quina M′dis in a que cuen e las ejecuciones de o ma más e icien e. Un ejemplo de caso en el que ocu e un enómeno simila es la de e minación de la can idad de núme os pa es meno que un cie o núme o cdado. Es e p oblema puede esol e se eco iendo odos los núme os meno es que cy decidiendo si son pa es (que en caso de es a ccodi icado en bina io conlle a un núme o exponencial de comp obacio- nes) o haciendo la di isión en e a de cen e 2, que es una ope ación cons an e en el amaño de la en ada. Desconocemos si exis e algún o o p ocedimien o, p esu- miblemen e más e icien e, que pueda con a el núme o de ce i icados sin e i ica ninguno. En caso de e i ica alguno, el hecho de que es e u ie a amaño exponen- cial espec o al amaño de la en ada implica ía que la comp obación no puede se ealizada en iempo polinómico. Dado que no se conoce un mé odo más e icien e de con a modelos pa a LT L ni pa a LP, pa ece azonable pensa que no exis i á pa a 34 Capí ulo 4. Conclusiones y T abajo Fu u o A lo la go del desa ollo de es e es udio, se ha podido obse a que algunas de las demos aciones p esen adas, en pa icula la del eo ema 3.2.3, son especialmen- e a duas an o de comp ende como de explica de mane a cla a y accesible. Es o e leja la p o undidad y la so is icación inhe en e a es os emas, lo que sub aya la necesidad de una mayo a ención y es udio especializado en es os aspec os de la eo ía de la complejidad y las lógicas empo ales. En es e abajo se ha o ecido po p ime ez has a donde sabemos un análisis de dis in as e siones de model coun ing en LT L⋄pa a modelos de amaño k. A modo de esumen se mues a una abla con odos los esul ados ob enidos, donde el esul ados de no pe enencia de palab as pe iódicas con kbina io a #P es á condicionado a la hipó esis de e i icación necesa ia, que indica que cada ejecución en una máquina de Tu ing que acep a debe codi ica un modelo álido y los esul ados de no pe enencia de k-á boles y k-g a os a alguna clase de equi alencia dependen de la hipó esis de almacenamien o necesa io, una suposición más exigen e que la an e io : kuna io kbina io Palab as pe iódicas co a in e io #P-comple o no en #P co a supe io #PSPACE k-á boles co a in e io no en #PSPACE no en #EXPSPACE co a supe io #EXPTIME #2EXPTIME k-g a os co a in e io #P-comple o no en #PSPACE co a supe io #EXPTIME En p ime luga , des acan las simili udes en e las complejidades de los modelos basados en palab as pe iódicas y k-g a os, simili ud azonable si enemos en cuen a que ambos ienen el mismo núme o de nodos. El caso de modelos basados en k-g a os es una gene alización del caso de palab as pe iódicas, lo cual jus i ica el aumen o de complejidad al conside a kcodi icado en bina io. Po o a pa e, los modelos basados en k-á boles ienen un núme o exponencialmen e mayo de nodos, po lo que esul a azonable que sean más complejos compu acionalmen e. Al obse a la abla, se obse an pocos esul ados de comple i ud, y los que se ienen son en #P, la clase de complejidad más es udiada de las que apa ecen en es e abajo y co a in e io de la complejidad de cualquie model coun ing en lógicas empo ales po se es as gene alización de la lógica p oposicional usual. Es o se debe a la escasez de p oblemas #PSPACE-comple os y #EXPSPACE- comple os conocidos a pa i de los cuales hace educciones pa simónicas pa a de- mos a la du eza de los p oblemas que se han es udiado. Una al e na i a al uso de educciones pa simónicas es el algo i mo usado en la demos ación del eo ema 35 3.2.3, que codi ica las ins ucciones y con igu aciones de la máquina de Tu ing que se necesi e en cada caso usando LT L⋄. Sin emba go, el au o no ha encon ado una mane a de hace lo, po lo que queda como abajo u u o. Se especula que, al encon a es a aducción pa a el caso en el que los modelos es án o mados po palab as pe iódicas de longi ud k, donde k es á codi icado en bina io, se á sencillo p oba la comple i ud pa a o as clases en el caso de modelos basados en k-á boles y k-g a os empleando aducciones simila es. Además, los esul ados elacionados con la no pe enencia a una de e minada clase del con eo de modelos que sa is acen una ó mula en LT L⋄es án condicio- nados po la inexis encia de un algo i mo de con eo más e icien e que el mé odo explíci o ac ualmen e conocido, como se ha mencionado an es. Es e mé odo equie- e que cada ejecución de una máquina de Tu ing conside e de mane a conc e a cada in e p e ación posible y la alide. De e mina si la hipó esis de e i icación necesa ia es cie a, ya sea median e una demos ación igu osa o a a és de la con adicción de dicha hipó esis, es un paso esencial pa a comple a es e abajo. Cap´ ı ulo 5 In oduc ion 5.1. Mo i a ion The objec i e o ma hema ics, and science in gene al, is o de ine and explain he eali y ha su ounds us. Na u al language is commonly used o explain wha happens a ound us, bu i is ull o exagge a ions, complexi ies and sub le ies which make i di icul o pe o m a de ailed s udy. Fo his eason, o mal languages ha e been c ea ed. They acili a e he objec i e exp ession o si ua ions and phenomena. Among o mal languages, he ones ha include ime as a a iable a e specially use ul when desc ibing physical phenomena. Fo ha pu pose, se e al empo al logics ha e been de ined, among which linea - ime empo al logic o LT L, a logic ha conside s ime as a linea lux, s ands ou . To o malise his kind o easoning and de e mine whe he a logical a i ma ion is ue (o i i could be) is a ele an p oblem in ma hema ics and compu a ion. The p oposi ional sa is iabili y p oblem (SAT), which conside s whe he , o a ce - ain o mula, he e is an in e p e a ion o u h alues o p oposi ions which make i ue, is esponsible o he c ea ion o hhe compu a ional complexi y analysis ield. O iginally, he analysis o he complexi y o empo al logic o mulas’sa is iabli y was pe o med in Sis la y Cla ke (1985). O he au ho s, such as Schnoebelen (2002), ha- e esea ched a ia ions o his p oblem, al e ing he empo al logics’seman ics o analysing di e en models and a ia ions o he sa is iabili y p oblem. Associa ed wi h he boolean sa is iabili y p oblem, we can de ine a coun ing p o- blem, which analyses he o al numbe o in e p e a ions ha sa is y a gi en o mula, is de ined. I is closely ela ed o p obabili y calcula ions and i is use ul o de e mine i a o mula ends o be ue. Coun ing complexi y in models o empo al logics was analysed in To ah y Zimme mann (2014), whe e he compu a ional complexi y o he sa is iabili y p oblem o LT L was explo ed. This esul ed in an idea o expand analogous esul s o o he logics whose complexi y has no been s udied as o now. 37 38 Capí ulo 5. In oduc ion 5.2. Resea ch objec i es The objec i e o his Bachelo ’s hesis is o analyse he complexi y associa ed wi h coun ing models ha sa is y a LT L o mula. These esul s a e mean o be used o sol e analogous p oblems wi h LT L⋄ o mulas. LT L⋄is a empo al logic s ic ly con ained wi hin LT L. Ano he objec i e is o inc ease unde s anding ega ding empo al logics and complexi y easonings, mainly ela ed wi h coun ing complexi y. 5.3. Wo king plan This s udy was di ided in o wo s ages: 1. Resea ch: Fi s , coun ing complexi y classes we e s udied, using chap e 17 o A o a y Ba ak (2006) as a s a ing poin , as ecommended by he u o s. A e wa ds, spa io- empo al easonings we e esea ched o o malise he p o- blem associa ed wi h de e mining he numbe o likely pas s o gi en p esen si ua ions. The objec i e was o analyse he complexi y o he easible pas de e mina ion p oblem o applied cases. Following a mee ing wi h he u o s, i was decided o expand and gene alise ou ocus o analyze empo al logics’complexi y. Wi h his new objec i e, a li e a u e esea ch ega ding he complexi y o coun ing p oblems in empo al logics. A e inding, eading and unde s anding he a icle w i en by To ah y Zimme mann (2014), i was ag eed o in es iga e he complexi y o coun ing he solu ions o o mulas in LT L⋄. 2. De elopmen : Once he esea ch objec i e was se led, he esul s ob ained by o he au ho s ega ding he complexi y o model coun ing in LT L o mulas we e used as a base o his s udy. New esul s abou he complexi y o he p oblem o coun ing he numbe o models o o mulas LT L⋄we e deduced and p o en. Pa icula ly, h ee di e en ypes o models in which sa is iabili y is de e mi- nis ic we e de e mined. An analysis o he complexi y o coun ing he numbe o each model ype ha sa is ied a o mula in LT L⋄. 5.4. Wo k s uc u e The es o his s udy is di ided in 5 chap e s, ollowing he s uc u e p esen ed below: 1. The chap e 2 ac s as a p e ace. I in oduces necessa y concep s o unde s and he s uc u e and esul s ound in he nex chap e . Rele an complexi y classes (and a hie a chy among hem) and he di e en logics ha will be used as a base o he s udy a e de ined. 5.4. Wo k s uc u e 39 2. The chap e 3 includes he bulk o his Bachelo ’s hesis. I con ains he au ho ’s wo k, some new p o en esul s and simila esul s ound by o he au ho s. 3. The chap e 4 consis s o a b ie summa y o he esul s ound in he p e ious chap e , hei analysis and u u e wo k possibili ies. 4. Finally, chap e s 5 y 6 a e English ansla ions o chap e s 1 and 4, espec i ely. Cap´ ı ulo 6 Conclusions and Fu u e Wo k The analysis o compu a ional complexi y is undamen al o ying o unde s- and inhe en di e ences be ween a ious p oblems and algo i hms. This analysis allows us o compa e he e iciency o algo i hms in e ms o ime and space equi- ed o hei execu ion. I also helps us iden i y he mos challenging p oblems and seek mo e e icien solu ions o hem. Addi ionally, as men ioned in he in oduc ion, he o malisa ion o empo al easoning is ex emely use ul o add ess issues ela ed o physical phenomena. Kno- wing he compu a ional complexi y o de e mining whe he a o malised physical easoning can be ue is essen ial in a g ea numbe o si ua ions. This complexi y can in luence ields whe e p ecision and e iciency a e c ucial, such as physics, engi- nee ing, o compu e science. Fu he mo e, i is highly use ul o be able o de e mine he p obabili y ha a ce ain e en will occu in he u u e o has occu ed in he pas , which can be i ially calcula ed by coun ing he numbe o si ua ions in which his e en a- kes place i each si ua ion has he same p obabili y. In any o he case, a simila easoning o coun ing pa hs will be equi ed. The basic capaci y o coun ing he numbe o si ua ions in which some hing happens is he e o e necessa y. This abi- li y is no only impo an in scien i ic and echnological applica ions, bu also in daily decision-making and isk assessmen , whe e unde s anding p obabili ies can signi ican ly enhance ou judgemen s and decisions. Conside ing his, we can unde s and ha he s udy o LT L and LT L⋄is ex e- mely in e es ing and ele an ac oss mul iple ields o knowledge. These logics ha e impo an applica ions in a eas such as sys em e i ica ion, a i icial in elligence, and dynamic sys ems heo y, among o he s. Howe e , hei unde s anding is com- plex and no comp ehensi ely co e ed in he cu iculum o his deg ee. Simila ly, he classes o coun ing complexi y, which a e essen ial o unde s anding he inhe en di icul y o coun ing p oblems, a e no pa o he usual cou se con en nei he , no a e many o he decision classes discussed in his p ojec . 41 42 Capí ulo 6. Conclusions and Fu u e Wo k Th oughou he de elopmen o his s udy, i has been obse ed ha some o he p esen ed demons a ions, pa icula ly ha o Theo em 3.2.3, a e especially a - duous o comp ehend and o explain clea ly and accessibly. This e lec s he dep h and sophis ica ion associa ed o hese opics. Fu he mo e, i also highligh s he need o g ea e a en ion and specialised s udy in hese aspec s o complexi y heo y and empo al logics. In his wo k, we ha e o e ed, o he bes o ou knowledge, he i s analysis o di e en e sions o model coun ing in LT L⋄ o models o size k. A summa y able wi h all he ob ained esul s is p esen ed below: una y kbina y k Pe iodic wo ds lowe bound #P-comple e no in #P uppe bound #PSPACE k- ees lowe bound no in #PSPACE no in #EXPSPACE uppe bound #EXPTIME #2EXPTIME k-g aphs lowe bound #P-comple e no in #PSPACE uppe bound #EXPTIME Bea in mind ha e e y esul o non-inclusion o a ce ain class p esen ed in he able abo e depends on he u h ulness o a ce ain hypo hesis. Fi s o all, pe io- dic wo ds wi h bina y kno belonging o #P depends o he manda o y e i ica ion hypo hesis. The esul s o non-inclusion o k-g aphs and k- ees depend on a second mo e es ic i e hypo hesis, he manda o y s o age hypo hesis. Fi s o all, he simila i ies be ween he complexi ies o models based on pe iodic wo ds and k-g aphs a e no ewo hy. This simila i y is easonable conside ing ha bo h ypes o models ha e he same numbe o nodes. The case o models based on k-g aphs is a gene alisa ion o he case o pe iodic wo ds. This jus i ies he inc ease in complexi y when conside ing kencoded in bina y. On he o he hand, models based on k- ees ha e an exponen ially la ge numbe o nodes, which explains hem being mo e compu a ionally complex. Upon examining he able, ew esul s o comple eness a e obse ed. Those ha do exis a e in #P, he mos s udied complexi y class among he ones men ioned in his a icle. Mo eo e , since model coun ing o empo al logics is a gene alisa ion o model checking o he usual p oposi ional logic, #P is he lowe bound o he complexi y o any o hese models. This sca ci y is due o he limi ed numbe o known #PSPACE-comple e and #EXPSPACE-comple e p oblems, om which pa simonious educ ions can be made o demons a e he ha dness o he s udied p oblems. An al e na i e o pa simonious educ ions is he algo i hm used in he demons a ion o Theo em 3.2.3, which en- 43 codes he ins uc ions and con igu a ions o he necessa y Tu ing machine in each case using LT L⋄. Howe e , he au ho has no ound a way o achie e his, lea ing i as u u e wo k. I is specula ed ha inding he ansla ion o models consis ing o pe iodic wo ds o leng h k, whe e kis encoded in bina y, will make i easie o p o e com- ple eness o o he classes o models based on k- ees and k-g aphs using simila ansla ions. Mo eo e , he esul s ela ed o he non-membe ship o a pa icula coun ing class o models ha sa is y a o mula in LT L⋄a e condi ioned by he lack o a mo e e icien coun ing algo i hm han he cu en ly known explici me hod. The explici me hod equi es ha each execu ion o a Tu ing machine conside s each possible in e p e a ion conc e ely and in de ail. De e mining he u h ulness o his assump ion, ei he h ough igo ous demons a ion o by con adic ing he hypo he- sis, is an essen ial s ep o comple e and s eng hen he p esen wo k.