Abstract FR:

Nous étudions la décidabilité et l'expressivité de mu-calcul propositionnel aussi bien avec des sémantiques linéaires qu'arborescentes. En particulier, nous nous intéressons a une logique pour la description de processus et de leurs propriétés appelée LSP et a ses extensions LSPA et LP. LSP est un mu-calcul à sémantique arborescente qui peut être vu comme une extension d'une algèbre de processus réguliers. Cette logique ainsi que ses extensions sont adéquates et expressive pour la bisimulation forte. Nous montrons la décidabilité de LSP par réduction au problème du langage vide des automates d'arbres infinis de Rabin. L'expressivité de LSP est comparée aux logiques du temps linéaire et arborescent. Nous montrons que LSP est équivalente au mu-calcul propositionnel de kozen. Par ailleurs, nous montrons que LSP est plus puissante que la classe des langages oméga réguliers et nous donnons une transformation qui associe a chaque formule d'une logique du temps linéaire une formule équivalente dans LSP