Scott A. Smolka Statement of Accomplishments February 2015 Scott A. Smolka has made fundamental contributions in the areas of process algebra, model checking, probabilistic processes, and cardiac-cell modeling and analysis. 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 150 publications, generating more than 7,000 citations. He has also been PI/Co-PI on grants totaling more than $18M. 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 --------------------------------------- In CAV 1994, Oleg Sokolsky and Smolka presented the first incremental algorithm for model checking. The algorithm 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. In CAV 1995, Sokolsky and Smolka presented first local model-checking algorithm for real-time systems. It computes, on-the-fly, a state-space quotient that is as coarse as possible with respect to clock constraints appearing in logical formula or timed automaton under investigation. In a 1994 LICS paper, Smolka, Sokolsky and Shipei Zhang were first to examine the parallel complexity of model checking. They 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 the formula or LTS results in membership in NC. Efficient NC-algorithms were presented for two versions of the problem involving alternation-free formulas. In 2005, he co-authored a TACAS paper with Radu Grosu describing first randomized, Monte Carlo algorithm for model checking. It uses random sampling of lassos (paths through a Buechi automaton ending in a cycle) to either reveal a counter-example, or to compute confidence interval bounding probability of finding a counter-example through further sampling. The number of samples taken is optimal. In TACAS 2011, Smolka and co-authors introduced the problem of Model Repair for probabilistic systems. Using a new version of parametric probabilistic model checking, they showed how the Model Repair problem can be reduced to a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique. 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 1990 IFIP Conference paper, Smolka and co-authors Alessandro Giacalone and Chi-Chang Jou introduced first probabilistic process algebra, PCCS, a probabilistic extension of Milner's SCCS. They also introduced notion of "epsilon bisimulation", and associated metric space for "deterministic" probabilistic processes, which became the basis for emerging notions of approximate bisimulation. Smolka continued his work in probabilistic process algebra by co-authoring 1995 I&C paper with Jos Baeten and Jan Bergstra on first probabilistic version of the ACP process algebra, including complete axiomatization of probabilistic bisimulation for finite-state processes. He also joined forces with Rance Cleaveland and Amy Zwarico to present in a 1999 I&C paper (preliminary versions appeared ICALP 1992 and CONCUR 1994) a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with 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 I&C paper on Reactive, Generative, and Stratified Models of Probabilistic Processes (preliminary version in LICS 1990). Additionally, he co-authored 1997 TCS paper with Sue Wu and Eugene Stark that introduced Probabilistic I/O Automata model of probabilistic processes. Modeling and Analysis of Cardiac Cells Using Hybrid Automata ------------------------------------------------------------ In a collection of papers, including 2008 Journal of Systems Biology, 2009 TCS, and 2007-2008 HSCC, Smolka in collaboration with Grosu and others introduced an efficient modeling framework for excitable cells based on Cycle-Linear Hybrid Automata: a new form of HA that exhibit linear behavior on a per-cycle basis, but whose overall behavior is nonlinear. CLHA accurately capture action-potential morphology and other typical excitable-cell characteristics; they also exhibit significantly improved computational efficiency in modeling complex wave patterns, including spiral waves underlying pathological conditions in the heart. In 2009 CACM paper, Smolka and co-authors introduced spatial-logic model checking to specify and detect emergent behavior e.g. spirals in networks of cardiac myocytes. Their logic is based on spatial superposition, and they devised method for learning formulae of this logic from spatial patterns under investigation. In CAV 2011, Smolka and co-authors performed first automated formal analysis of a realistic cardiac cell model, the Minimal Model of Fenton et al. The analysis involved determining parameter ranges that lead to loss of excitability, a precursor to various cardiac arrhythmic disorders. Key to the approach was to first transform Fenton's model into a multiaffine HA, thereby allowing techniques developed for Genetic Regulatory Networks to be used to identify parameter ranges of interest. In HSCC 2014, Smolka and co-authors were first to use compositional reasoning in feedback-based biological setting, showing how the sodium-channel component of a detailed cardiac-cell model can be replaced with a much simpler approximately bisimilar Hodgkin-Huxley abstraction.