Scott A. Smolka Statement of Accomplishments July 2010 Scott Smolka has made fundamental contributions in the areas of process algebra, model checking, and models of probabilistic processes and excitable cells. He is perhaps best known for the algorithm he and Paris Kanellakis invented for deciding bisimulation. Smolka's research in these areas has resulted in over 140 publications. He has also been the PI or Co-PI on grants totaling more than $17M. Deciding Bisimulation --------------------- The main result of the Kanellakis and Smolka 1990 Information and Computation article on ``CCS Expressions, Finite State Processes, and Three Problems of Equivalence'', an extended version of a 1983 PODC paper, is what has come to be known as the K-S Relational Coarsest Partitioning algorithm. The K-S algorithm can be used to efficiently decide bisimulation equivalence, a cornerstone of Milner's CCS and other process-algebraic formalisms, in polynomial time. Observational equivalence, a notion of process equivalence closely related to bisimulation, can be defined as the limit of a sequence of successively finer equivalence relations, k-approximation, where 1-approximation is NFA equivalence. Kanellakis and Smolka also showed that, for each fixed k, deciding k-approximation is PSPACE-complete. They further showed that testing for failure equivalence, a notion of process equivalence central to Brookes, Hoare and Roscoe's CSP, is PSPACE-complete, even for a very restricted type of process. Efficient Algorithms for Model Checking --------------------------------------- Smolka's main contributions to the field of model checking include the CAV 1994 and 1995 papers he co-authored with Oleg Sokolsky on the first incremental algorithm for model checking, and the first local model-checking algorithm for real-time systems. In a 1994 LICS paper, Smolka and Sokolsky, along with Shipei Zhang, were the first to examine the parallel complexity of model checking. In 2005, he co-authored a TACAS paper with Radu Grosu describing the first randomized, Monte Carlo algorithm for model checking. The incremental algorithm for model checking takes as input a set Delta of "changes" to the labeled transition system (LTS) under investigation, where a change constitutes an inserted or deleted transition. The algorithm requires time linear in the size of the LTS in the worst case, but only time linear in Delta in the best case. The main novelty of the local algorithm for model checking real-time systems is that it computes, on-the-fly, a state-space quotient that is as coarse as possible with respect to the clock constraints appearing in the logical formula or timed automaton used to represent the system under investigation. The 1994 LICS paper showed that the problem of checking whether an LTS is a model of a formula of the propositional modal mu-calculus is P-complete even for a very restrictive version of the problem involving the alternation-free fragment. This result is tight in the sense that placing any further non-trivial restrictions on either the formula or LTS results in membership in NC. Specifically, efficient NC-algorithms were presented for two versions of the problem involving alternation-free formulas over a constant number of fixed-point operators. The Monte Carlo model-checking algorithm uses random sampling of lassos (paths through a Buechi automaton ending in a cycle) to either reveal a counter-example in the form of an accepting lasso, or to compute a confidence interval bounding the probability of finding an accepting lasso through further sampling. The number of samples taken is optimal. Probabilistic Process Algebra and Models of Probabilistic Processes ------------------------------------------------------------------- Smolka has also made fundamental contributions in the areas of probabilistic process algebra and models of probabilistic processes. In a 1990 IFIP Conference paper, Smolka and co-authors Alessandro Giacalone and Chi-Chang Jou introduced the first probabilistic process algebra in PCCS, a probabilistic extension of Milner's SCCS. They also introduced the notion of "epsilon bisimulation", and an associated metric space for "deterministic" probabilistic processes, which became the basis for emerging notions of approximate bisimulation for labeled Markov chains. Smolka continued his work in probabilistic process algebra by co-authoring a 1995 Information and Computation paper with Jos Baeten and Jan Bergstra on the first probabilistic version of the ACP process algebra, including a complete axiomatization of probabilistic bisimulation for finite-state processes. He also joined forces with Rance Cleaveland and Amy Zwarico to present in a 1999 Information and Computation paper (preliminary versions of which appeared in 1992 ICALP and 1994 CONCUR papers) a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with the classical testing theory of De Nicola and Hennessy in that whenever a process passes a test with probability 1 (respectively some non-zero probability) in this new setting, then the process "must" (respectively "may") pass the test in the classical theory. In the area of probabilistic processes, Smolka co-authored, with Rob van Glabbeek and Bernhard Steffen, the highly cited 1995 Information and Computation paper on Reactive, Generative, and Stratified Models of Probabilistic Processes (a preliminary version of which appeared in LICS 1990). Additionally, he co-authored a 1997 Theoretical Computer Science paper with Sue Hwey Wu and Eugene Stark that introduced the Probabilistic I/O Automata model of probabilistic processes. Efficient Modeling of Excitable Cells Using Hybrid Automata ----------------------------------------------------------- In a collection of papers that includes those appearing in 2008 Journal of IET Systems Biology, 2009 Theoretical Computer Science, and 2007-2008 HSCC, Smolka and co-authors Emilia Entcheva, Radu Grosu, and others, introduced an efficient modeling framework for excitable cells based on Cycle-Linear Hybrid Automata. CLHA are a new form of Hybrid Automata that exhibit linear behavior on a per-cycle basis but whose overall behavior is nonlinear. They accurately capture action-potential morphology and other typical excitable-cell characteristics such as refractoriness and restitution. CLHA-based simulation frameworks exhibit significantly improved computational efficiency in modeling complex wave patterns, such as the spiral waves underlying pathological conditions in the heart. In a 2009 CACM paper, Smolka and co-authors introduced spatial logic model checking to specify and detect emergent behavior such as spirals in networks of cardiac myocytes. Their new spatial logic is based on spatial superposition, and they devised a method for learning the formulae of this logic from the spatial patterns under investigation.