%0 Journal Article %J Knowledge and Data Engineering, IEEE Transactions on %D 2012 %T A Temporal Pattern Search Algorithm for Personal History Event Visualization %A Wang,T. D %A Deshpande, Amol %A Shneiderman, Ben %K automaton-based approach %K binary search %K bit-parallel approach %K data visualisation %K electronic health records %K event array %K finite automata %K interactive visualization program %K Lifelines2 visualization tool %K medical information systems %K NFA approach %K nondeterministic finite automaton %K O(m2n lg(n)) problem %K pattern matching %K personal history event visualization %K Shift-And approach %K temporal pattern search algorithm %K time stamp %X 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. %B Knowledge and Data Engineering, IEEE Transactions on %V 24 %P 799 - 812 %8 2012/05// %@ 1041-4347 %G eng %N 5 %R 10.1109/TKDE.2010.257 %0 Conference Paper %B , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings %D 1995 %T Efficient on-the-fly model checking for CTL %A Bhat,G. %A Cleaveland, Rance %A Grumberg,O. %K Algorithm design and analysis %K Automata %K computational complexity %K Computer science %K CTL %K Encoding %K finite automata %K finite-state system %K global algorithm %K Logic %K LTL %K on-the-fly model checking %K Performance analysis %K Safety %K State-space methods %K sublogic %K temporal logic %K time complexity %X 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 %B , Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings %I IEEE %P 388 - 397 %8 1995/06/26/29 %@ 0-8186-7050-9 %G eng %R 10.1109/LICS.1995.523273 %0 Conference Paper %B Real-Time Systems Symposium, 1994., Proceedings. %D 1994 %T Verifying an intelligent structural control system: a case study %A Elseaidy,W. M %A Cleaveland, Rance %A Baugh,J. W. %K automatic verification tool %K case study %K Concurrency Workbench %K Distributed computing %K Distributed control %K distributed processing %K finite automata %K finite-state processes %K formal verification %K graphical specification language %K high-level design %K intelligent control %K intelligent structural control system verification %K Logic %K Modechart %K Process algebra %K Real time systems %K real-time systems %K Specification languages %K structural engineering computing %K temporal logic %K temporal process algebra %K time-varying systems %K Timing %K timing properties %K visual languages %X 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 %B Real-Time Systems Symposium, 1994., Proceedings. %I IEEE %P 271 - 275 %8 1994/12/07/9 %@ 0-8186-6600-5 %G eng %R 10.1109/REAL.1994.342708