K. Etessami, E. Martinov, A. Stewart, and M. Yannakakis, "Reachability for Branching Concurrent Stochastic Games". Preprint: ArXiv:1806.03907, 2018.

K. Etessami, A. Stewart, and M. Yannakakis,
"Greatest Fixed Points of Probabilistic Min/Max Polynomial Equations, and Reachability for Branching Markov Decision Processes". Conference version in
* Proc. of 42nd Int. Coll. on Automata, Languages and Programming (ICALP'15)*.
Preprint:
ArXiv:1502.05533, 2015.

K. Etessami, "The complexity of computing a (quasi-)perfect equilibrium for an n-player extensive form game of perfect recall" (submitted), 2014. Preprint: ArXiv:1408.1233 .

K. Etessami, K. A. Hansen, P. B. Miltersen, T. B. Sorensen,
"The complexity of approximating a trembling hand perfect equilibrium of a multi-player game in strategic form".
Conference version in *Proc. of 7th Int. Symp. on Algorithmic Game Theory (SAGT'14)*, 2014. Preprint:
ArXiv:1408.1017.

(* Survey (DRAFT): *) K. Etessami
"Analysis of Probabilistic Processes and Automata Theory".
DRAFT of Chapter in forthcoming *Handbook of Automata Theory*,
editor Jean-Eric Pin, European Mathmatical Society publishing (EMS), to appear in 2015 (??).

K. Etessami, A. Stewart, and M. Yannakakis,
"A note on
the complexity of comparing succinctly represented integers,
with an application to maximum probability parsing".
*ACM Transactions on Computation Theory*, volume 6 (2), 2014.
Preprint:
ArXiv:1302.6411, 2013.

K. Etessami, A. Stewart, and M. Yannakakis,
"Stochastic Context-Free Grammars, Regular Languages,
and Newton's Method", Conference version
in *ICALP'2013*,
Preprint:
ArXiv:1302.6411, 2013.

A. Stewart, K. Etessami, and M. Yannakakis,
"Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata", to appear in *Journal of the ACM*, 2015.
(Conference version appeared in *CAV'2013*.)
Preprint:
arXiv:1302:3741, 2013.

K. Etessami, A. Stewart, and M. Yannakakis,
"Polynomial-time Algorithms for Branching Markov Decision Processes and
Probabilistic Min(Max) Polynomial Bellman Equations", manuscript 2012 .
Conference version in
* Proc. of 39th Int. Coll. on Automata, Languages and Programming (ICALP'12)*, 2012.
Preprint:
ArXiv:1202.4798.

K. Etessami, A. Stewart, and M. Yannakakis,
"Polynomial-time Algorithms for Multi-type Branching
Processes and Stochastic Context-Free Grammars", manuscript
2011.
Conference version in *Proc. 44th ACM Symp. on Theory
of Computing (STOC'12), 2012*.
Preprint:
ArXiv:1201.2374.

T. Brazdil, V. Brozek, K. Etessami, and T. Kucera,
"Approximating the Termination value of One-counter MDPs and Stochastic
Games",
Journal
version in * Information and Computation *, volume 222, pp. 121-138, 2013.
full preprint (of the journal version) available here.
Conference version in * Proc. of 38th Int. Coll. on Automata, Languages and Programming (ICALP'11)*, pages 332-343, 2011.

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.
*Performance Evaluation*, volume 67(9), pages 837-857, 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, in Logical Methods in Computer Science (LMCS), volume 4(4), 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.

See the full journal paper,
to appear in Journal of the ACM
(70 pages), 2015.
The journal paper combines the results of both our ICALP'05 paper (see below) and this STACS'06 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 Transactions on
Computational Logic,
available
electronically here,
together with an electronic appendix available here (2012).
The full journal 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,
to appear in Journal of the ACM, 70 pages, 2015.
Conference version
appeared in
32nd
Int. Coll. on
Automata, Languages and Programming (ICALP'05), 2005.

The journal version (to appear in JACM, 2015)
combines the results of both this ICALP'05 paper and our STACS'06 paper
(see above).

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 (2012),
(available
electronically here),
together with an electronic appendix available here.
The journal 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.