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.