Selected publications by Paul Gastin

V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64(2), pages 396-418, 2002. ( PS | PS.GZ )

Abstract:: A long standing open problem in the theory of (Mazurkiewicz) traces has been the question whether LTL (Linear Temporal Logic) is expressively complete with respect to the first order theory. We solve this problem positively for finite and infinite traces and for the simplest temporal logic, which is based only on next and until modalities. Similar results were established previously, but they were all weaker, since they used additional past or future modalities. Another feature of our work is that our proof is direct and does not use any reduction to the word case.

`@article{DiGa02jcss,`
	`author =`	`{Diekert, Volker and Gastin, Paul},`
	`journal =`	`{Journal of Computer and System Sciences},`
	`month =`	`mar,`
	`number =`	`{2},`
	`pages =`	`{396-418},`
	`publisher =`	`{Elsevier Science Publishers},`
	`title =`	`{{LTL} is expressively complete for {M}azurkiewicz traces},`
	`url =`	`{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JCSS02dg.ps},`
	`volume =`	`{64},`
	`year =`	`{2002},`
`}`

About LSV