I was born in Fundão, Portugal, in 1978. I graduated in Mathematics at UBI in July 2002, and I got a MSc in Pure Mathematics at FCUL in 2005. My Master thesis M-solid Varieties of Languages was supervised by Professora Margarita Ramalho. I was a member of Center of Algebra of the University of Lisbon, from March 2004 to October 2005. I was a student member of the former Center for Logic and Computation since November 2005.

I am preparing my PhD thesis, on Model Checking of Quantum Systems under the supervision of Professor Paulo Mateus, with a scholarship from FCT.

Studied the application of the exogenous probabilistic logic EPPL [pmat:acs:css:05a] to probabilistic systems composed by a finite number of random variables, as probabilistic cellular automata, random fields and markovian networks. Implementing efficient model-checking techniques. Obtained a small model theorem and PSPACE SAT algorithm for the logic [pbtz:pmat:08].
Developing the exogenous temporal probabilistic logic EPLTL. Obtained a sound and complete Hilbert calculus and a model-checking procedure [pbtz:pmat:08], [pbtz:pmat:raja:nick:07].

Developing a temporal logic for quantum computational systems based in the state logic EQPL [pmat:acs:css:05a]. Obtained a complete Hilbert calculus [pbtz:rcha:pmat:08] and a model-checking algorithm [pbtz:rcha:pmat:acs:06]

• P. Baltazar. M-solid varieties of languages. Acta Cybernetica, 18(4):719--731, 2008.  [05-B-msolid.pdf]

• P. Baltazar, R. Chadha, P. Mateus, and A. Sernadas. Towards model-checking quantum security protocols. In P. Dini et al, editor, Proceedings of the First Workshop on Quantum Security: QSec'07, page 0014. IEEE Press, 2007. [06-BCMS-quantlog13s.pdf]

• P. Baltazar, P. Mateus, R. Nagarajan, and N. Papanikolaou. Exogenous probabilistic computation tree logic.Electronic Notes in Theoretical Computer Science, 190(3):95--110, 2007.   [07 BMNP-quantlog15s.pdf]
• All