TY - JOUR
T1 - A Temporal Pattern Search Algorithm for Personal History Event Visualization
JF - Knowledge and Data Engineering, IEEE Transactions on
Y1 - 2012
A1 - Wang,T. D
A1 - Deshpande, Amol
A1 - Shneiderman, Ben
KW - automaton-based approach
KW - binary search
KW - bit-parallel approach
KW - data visualisation
KW - electronic health records
KW - event array
KW - finite automata
KW - interactive visualization program
KW - Lifelines2 visualization tool
KW - medical information systems
KW - NFA approach
KW - nondeterministic finite automaton
KW - O(m2n lg(n)) problem
KW - pattern matching
KW - personal history event visualization
KW - Shift-And approach
KW - temporal pattern search algorithm
KW - time stamp
AB - We present Temporal Pattern Search (TPS), a novel algorithm for searching for temporal patterns of events in historical personal histories. The traditional method of searching for such patterns uses an automaton-based approach over a single array of events, sorted by time stamps. Instead, TPS operates on a set of arrays, where each array contains all events of the same type, sorted by time stamps. TPS searches for a particular item in the pattern using a binary search over the appropriate arrays. Although binary search is considerably more expensive per item, it allows TPS to skip many unnecessary events in personal histories. We show that TPS's running time is bounded by O(m2n lg(n)), where m is the length of (number of events) a search pattern, and n is the number of events in a record (history). Although the asymptotic running time of TPS is inferior to that of a nondeterministic finite automaton (NFA) approach (O(mn)), TPS performs better than NFA under our experimental conditions. We also show TPS is very competitive with Shift-And, a bit-parallel approach, with real data. Since the experimental conditions we describe here subsume the conditions under which analysts would typically use TPS (i.e., within an interactive visualization program), we argue that TPS is an appropriate design choice for us.
VL - 24
SN - 1041-4347
CP - 5
M3 - 10.1109/TKDE.2010.257
ER -
TY - CONF
T1 - Efficient on-the-fly model checking for CTL
T2 - , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings
Y1 - 1995
A1 - Bhat,G.
A1 - Cleaveland, Rance
A1 - Grumberg,O.
KW - Algorithm design and analysis
KW - Automata
KW - computational complexity
KW - Computer science
KW - CTL
KW - Encoding
KW - finite automata
KW - finite-state system
KW - global algorithm
KW - Logic
KW - LTL
KW - on-the-fly model checking
KW - Performance analysis
KW - Safety
KW - State-space methods
KW - sublogic
KW - temporal logic
KW - time complexity
AB - This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL. The time complexity of our algorithm matches that of the best existing “global algorithm” for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice
JA - , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings
PB - IEEE
SN - 0-8186-7050-9
M3 - 10.1109/LICS.1995.523273
ER -
TY - CONF
T1 - Verifying an intelligent structural control system: a case study
T2 - Real-Time Systems Symposium, 1994., Proceedings.
Y1 - 1994
A1 - Elseaidy,W. M
A1 - Cleaveland, Rance
A1 - Baugh,J. W.
KW - automatic verification tool
KW - case study
KW - Concurrency Workbench
KW - Distributed computing
KW - Distributed control
KW - distributed processing
KW - finite automata
KW - finite-state processes
KW - formal verification
KW - graphical specification language
KW - high-level design
KW - intelligent control
KW - intelligent structural control system verification
KW - Logic
KW - Modechart
KW - Process algebra
KW - Real time systems
KW - real-time systems
KW - Specification languages
KW - structural engineering computing
KW - temporal logic
KW - temporal process algebra
KW - time-varying systems
KW - Timing
KW - timing properties
KW - visual languages
AB - Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct
JA - Real-Time Systems Symposium, 1994., Proceedings.
PB - IEEE
SN - 0-8186-6600-5
M3 - 10.1109/REAL.1994.342708
ER -