Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 4 of 4
Full-Text Articles in Physical Sciences and Mathematics
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Research Collection School Of Computing and Information Systems
The process analysis toolkit (PAT) integrates the expressiveness of state, event, time, and probability-based languages with the power of model checking. PAT is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 12 different expressive modeling languages with many application domains and has attracted thousands of registered users from hundreds of organizations. In this invited talk, we will present the PAT system and its vision on “Event Analytics” (EA) which is beyond “Data Analytics”. The EA research is based on applying model checking to event planning, scheduling, prediction, strategy analysis and decision …
Gpu Accelerated Counterexample Generation In Ltl Model Checking, Zhimin Wu, Yang Liu, Yun Liang, Jun Sun
Gpu Accelerated Counterexample Generation In Ltl Model Checking, Zhimin Wu, Yang Liu, Yun Liang, Jun Sun
Research Collection School Of Computing and Information Systems
Strongly Connected Component (SCC) based searching is one of the most popular LTL model checking algorithms. When the SCCs are huge, the counterexample generation process can be time-consuming, especially when dealing with fairness assumptions. In this work, we propose a GPU accelerated counterexample generation algorithm, which improves the performance by parallelizing the Breadth First Search (BFS) used in the counterexample generation. BFS work is irregular, which means it is hard to allocate resources and may suffer from imbalanced load. We make use of the features of latest CUDA Compute Architecture-NVIDIA Kepler GK110 to achieve the dynamic parallelism and memory hierarchy …
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …
Towards Formal Modelling And Verification Of Pervasive Computing Systems, Yan Liu, Xian Zhang, Yang Liu, Jin Song Dong, Jun Sun, Jit Biswas, Mounir Mokhtari
Towards Formal Modelling And Verification Of Pervasive Computing Systems, Yan Liu, Xian Zhang, Yang Liu, Jin Song Dong, Jun Sun, Jit Biswas, Mounir Mokhtari
Research Collection School Of Computing and Information Systems
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of …