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 -