some publications

K. Etessami, A. Stewart, and M. Yannakakis, "Polynomial-time Algorithms for Multi-type Branching Processes and Stochastic Context-Free Grammars", manuscript 2011. Preprint: ArXiv:1201.2374.
Conference version to appear in Proc. 44th ACM STOC'2012.

T. Brazdil, V. Brozek, K. Etessami, and T. Kucera, Approximating the Termination value of One-counter MDPs and Stochastic Games, in Proc. of 38th Int. Coll. on Automata, Languages and Programming (ICALP'11), pages 332-343, 2011. Full version available here.

T. Brazdil, V. Brozek, and K. Etessami, One-Counter Stochastic Games, full preprint (20 pages), 2010. Conference version appeared in Proc. of Ann. Conf. on Foundations of Software Technology and theoretical computer science (FSTTCS'10), pages 108-119, 2010.

T. Brazdil, V. Brozek, K. Etessami, A. Kucera, D. Wojtczak, One-Counter Markov Decision Processes, Preprint: arXiv:0904.2511, 2009. In Proc. 21st ACM-SIAM Symp. on Discrete Algorithms (SODA'2010), 2010.

K. Etessami and P. Godefroid, An Abort-Aware Model of Transactional Programming, appeared in Proc. of 10th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), 2009. (Also a Microsoft Research Tech Report: MSR-TR-2008-159, 2008. A short Position Paper based on this work appeared earlier at the (EC)^2 Workshop, 2008.)

K. Etessami, D. Wojtczak, and M. Yannakakis, Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems. To appear in the journal Performance Evaluation, 2010. Conference version appeared in 5th Int. Conf. on Quantitative Evaluation of Systems (QEST'08), 2008.

K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM Journal on Computing, Vol. 39(6), pp. 2531--2597, 2010. The earlier conference version appeared in 48th IEEE Symp. on Foundations of Computer Science (FOCS), 2007.

K. Etessami, D. Wojtczak, and M. Yannakakis, Recursive Stochastic Games with Positive Rewards, Tech Report, U. of Edinburgh, EDI-INF-RR-1224, 2007. Conference version appeared in 35th Int. Coll. on Automata, Languages and Programming (ICALP'08), 2008.

R. Alur, M. Arenas, P. Barcelo, K. Etessami, N. Immerman, and L. Libkin, First-Order and Temporal Logics for Nested Words , in 22nd IEEE Symposium on Logic in Computer Science (LICS), 2007. Here is the Journal version, which appeared in Logical Methods in Computer Science (LMCS), volume 4(4): 2008.

K. Etessami, M. Kwiatkowska, M. Y. Vardi, and M. Yannakakis, Multi-Objective Model Checking of Markov Decision Processes, in 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), 2007. Here is the Journal version, to appear in Logical Methods in Computer Science (LMCS), 2008.

D. Wojtczak and K. Etessami PReMo: an analyzer for probabilistic recursive models, (short tool paper) in 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), 2007. Here is a longer version with some more experimental results in the appendix.

K. Etessami and M. Yannakakis, Recursive Concurrent Stochastic Games, in 33nd Int. Coll. on Automata, Languages and Programming (ICALP'06), 2006. Here is the Journal version, which appeared in Logical Methods in Computer Science (LMCS), volume 4(4): 2008.

K. Etessami and M. Yannakakis, Efficient Qualitative Analysis of classes of Recursive Markov Decision Processes and Simple Stochastic Games, in 23rd Symp. on Theoretical Aspects of Computer Science (STACS'06), 2006.
Here is the full journal submission (57 pages) which combines the results of both our ICALP'05 paper (see below) and this STACS'06 paper, which extended the results of the earlier paper.

M. Yannakakis and K. Etessami, Checking LTL properties of Recursive Markov Chains, in 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST'05), 2005.
The full version of this paper (60 pages) titled Model Checking of Recursive Probabilistic Systems, appears in the journal ACM Trans. on Computational Logic, available now electronically here, together with an electronic appendix available here (2011). The full version combines the results of both our TACAS'05 paper (see below) and this QEST'05 paper on the same topic.

K. Etessami and M. Yannakakis, Recursive Markov Decision Processes and Recursive Stochastic Games, in 32nd Int. Coll. on Automata, Languages and Programming (ICALP'05), 2005.
Here is the full journal submission (57 pages) which combines the results of both this ICALP'05 paper and our STACS'06 paper (see above) on the same topic.

K. Etessami and M. Yannakakis, Algorithmic Verification of Recursive Probabilistic State Machines. in 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), 2005.
The full version of this paper (60 pages) titled Model Checking of Recursive Probabilistic Systems, appears in the journal ACM Trans. on Computational Logic, (available electronically now here, together with an electronic appendix available here (2011). The full version combines the results of both this TACAS'05 paper and our QEST'05 paper (see above) on the same topic.

R. Alur, S. Chaudhuri, K. Etessami, P. Madhusudan, On-the-fly Reachability and Cycle Detection for Recursive State Machines, in 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), 2005.

J. Esparza and K. Etessami, Verifying Probabilistic Procedural Programs. In FSTTCS'04, December, 2004.(Invited early survey, for talk by Esparza. Briefly surveys our first paper [Etessami-Yannakakis,STACS'05] on Recursive Markov Chains, and also surveys Esparza, Kucera, et. al.'s work [LICS'04,STACS'05] on probabilistic Pushdown Systems.)

K. Etessami and M. Yannakakis, Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations. Journal of the Association for Computing Machinery (JACM) volume 56(1): January, 2009.
Here's the short conference version which appeared in 22nd Int. Symp. on Theoretical Aspects of Computer Science (STACS'05), 2005.

K. Etessami and A. Lochbihler, The Computational Complexity of Evolutionarily Stable Strategies. in Int. Journal of Game Theory, vol. 37 (1): 93--113, 2008. An earlier version was made available as a ECCC tech report TR04-055, 2004.

R. Alur, K. Etessami, and P. Madhusudan, A Temporal Logic of Nested Calls and Returns, In 10th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), 2004.

K. Etessami, Analysis of Recursive Game Graphs using Dataflow Equations In Proc. of 5th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VCMAI'04) , 2004.

R. Alur, S. Chaudhuri, K. Etessami, S. Guha, and M. Yannakakis. Compression of Partially Ordered Strings In Proc. of CONCUR'2003, Springer LNCS 2761, 2003.

K. Etessami. A hierarchy of polynomial-time computable simulations for automata. In Proc. of CONCUR'2002, Springer LNCS 2421, pages 131-144, 2002.

K. Etessami, Th. Wilke, and R. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM Journal on Computing, 34(5): 1159--1175, 2005.
Conference version appeared in Proc. of 28th Int. Col. on Automata, Languages, and Programming (ICALP'2001), Springer LNCS 2076, pages 694-707, 2001.

R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. Reps, and M. Yannakakis. Analysis of Recursive State Machines. in ACM Trans. on Programming Languages and Systems, 27(4): 786-818, 2005.
Conference version: R. Alur, K. Etessami, M. Yannakakis, Analysis of Recursive State Machines, In Proc. of 13th Conf. on Computer-Aided Verification (CAV'2001) , Springer LNCS 2102, pages 207-220, 2001.
(Journal paper joined with independent work of M. Benedikt, P. Godefroid, and T. Reps).

R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs. In Proc. of 28th Int. Col. on Automata, Languages, and Programming (ICALP'2001) . Full journal version appears Theoretical Computer Science, 2005.

K. Etessami and M. Yannakakis. From rule-based to automata-based testing. In Proc. of 20th IFIP Int. Conf. on Formal Description Techniques/Protocol Specification, Testing and Verification (FORTE/PSTV'2000), 2000.

K. Etessami. A note on a question of Peled and Wilke regarding stutter-invariant LTL, Information Processing Letters , vol. 75 (6), pp. 261-263, 2000.

K. Etessami and G. Holzmann. Optimizing Büchi automata, in Proc. of 11th Int. Conf. on Concurrency Theory (CONCUR'2000) , pp. 153-167, 2000.

R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts, Journal version appeared in IEEE Transactions on Software Engineering, 2003 , volume 29(7), pp. 623-633. Due to space limitations in the journal, here is the Full Version, more complete than the journal paper . Conference version appeared in Proc. of 22nd Int. Conf. on Software Engineering (ICSE'2000) , pp. 304-313, 2000.

R. Alur, K. Etessami, S. LaTorre, and D. Peled, Parametric temporal logic for model measuring , in ACM Transactions on Computational Logic , vol. 2 (3), pp. 388-407, 2001. Conference version appeared in Proc. of 26th Int. Coll. on . Automata, Languages, and Programming (ICALP'99), pp. 159-168, 1999.

K. Etessami, Stutter-invariant languages, omega-automata, and temporal logic, in Proc. of 11th Int. Conf. on Computer-Aided Verification (CAV'99) , pp. 236-248, 1999.

K. Etessami, Dynamic tree isomorphism via first-order updates to a relational database, in Proc. of 17th ACM Symp. on Principles of Database Systems (PODS'98) , 1998, pp. 235-243.

K. Etessami, M. Y. Vardi, and Th. Wilke First-order logic with two variables and unary temporal logic, Information and Computation , volume 179(2), pp. 279-295, 2002. Conference version appeared in Proc. of 12th IEEE Symp. on Logic in Computer Science (LICS'97) , pp. 228-235, 1997.

K. Etessami and Th. Wilke. An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic, Information and Computation , volume 160(1/2), pp. 88-108, 2000. Conference version appeared as "An Until Hierarchy for Temporal Logic" in Proc. of 11th IEEE Symp. on Logic in Computer Science (LICS'96) , pp. 108-117, 1996.

K. Etessami. Counting quantifiers, successor relations, and logarithmic space, Journal of Computer and System Sciences , volume 54(3), pp. 400-411, 1997. Conference version appeared in Proc. of 10th IEEE Structure in Complexity Theory Conference (Structures'95) , pp. 1-11, 1995.

K. Etessami and N. Immerman, Tree canonization and transitive closure, Information and Computation , volume 157(1/2), pp. 2-24, 2000. Conference version appeared in Proc. of 10th IEEE Symp. on Logic in Computer Science (LICS'95) , pp. 331-341, 1995.

K. Etessami and N. Immerman, Reachability and the power of local ordering, in Theoretical Computer Science , volume 149, pp. 227-260, 1995. Conference version appeared in 11th Symposium on Theoretical Aspects of Computer Science (STACS'94) , pp. 123-135, 1994.