Procédures de décision et expressivité dans la logique temporelle du temps ramifié

Dans cet article, nous considérons la Logique de l'Arbre de Computation (CTL) proposée dans CE, qui étend la Logique de Temps Ramifié Unifiée (UB) de BMP en ajoutant un opérateur jusqu'à ce que. Nous établissons que CTL possède la propriété petite en montrant que toute formule CTL satisfaisable est satisfaisable dans un petit modèle fini obtenu d'un petit « pseudo-modèle » résultant de la construction du quotient de Fischer Ladner. Nous proposons ensuite un algorithme en temps exponentiel pour décider de la satisfiabilité dans CTL et étendons l'axiomatisation de UB donnée dans BMP à une axiomatisation complète pour CTL. Enfin, nous étudions le pouvoir expressif relatif d'une famille de logiques temporelles obtenues en étendant ou en restreignant la syntaxe de UB et CTL.