Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Linear Temporal Logic (3)
- Model Check (3)
- Operational Semantic (2)
- Binary tree formation (1)
- Cooperative learning (1)
-
- GRASP (1)
- Hybrid Algorithm (1)
- Label Transition System (1)
- Liveness Property (1)
- Model Check Algorithm (1)
- Model Checker (1)
- Mutual Exclusion (1)
- Policy sharing (1)
- Process Construct (1)
- Quadratic Assignment Problem (1)
- Reinforcement learning (1)
- Simulated Annealing (1)
- Simulated annealing (1)
- State Object (1)
- State Reachability (1)
- Strongly Connect Component (1)
- Symbolic Model Check (1)
- Symmetry Reduction (1)
- Tabu Search (1)
- Tabu search (1)
- Teacher assignment (1)
- Timetabling problem (1)
- Topology-based multi-agent systems (1)
- Wireless Sensor Network (1)
Articles 1 - 8 of 8
Full-Text Articles in Physical Sciences and Mathematics
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li
Research Collection School Of Computing and Information Systems
Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We …
Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan
Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan
Research Collection School Of Computing and Information Systems
Topology-based multi-agent systems (TMAS), wherein agents interact with one another according to their spatial relationship in a network, are well suited for problems with topological constraints. In a TMAS system, however, each agent may have a different state space, which can be rather large. Consequently, traditional approaches to multi-agent cooperative learning may not be able to scale up with the complexity of the network topology. In this paper, we propose a cooperative learning strategy, under which autonomous agents are assembled in a binary tree formation (BTF). By constraining the interaction between agents, we effectively unify the state space of individual …
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu
Research Collection School Of Computing and Information Systems
Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled …
An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu
An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu
Research Collection School Of Computing and Information Systems
In inference of untimed regular languages, given an unknown language to be inferred, an automaton is constructed to accept the unknown language from answers to a set of membership queries each of which asks whether a string is contained in the unknown language. One of the most well-known regular inference algorithms is the L* algorithm, proposed by Angluin in 1987, which can learn a minimal deterministic finite automaton (DFA) to accept the unknown language. In this work, we propose an efficient polynomial time learning algorithm, TL*, for timed regular language accepted by event-recording automata. Given an unknown timed regular language, …
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Model checking has established itself as an effective system analysis method, as it is capable of proving/dis-proving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this work, we first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction. We extend the PAT model checker with the technique and demonstrate its usability by verifying recently …
Solving The Teacher Assignment Problem By Two Metaheuristics, Aldy Gunawan, Kien Ming Ng
Solving The Teacher Assignment Problem By Two Metaheuristics, Aldy Gunawan, Kien Ming Ng
Research Collection School Of Computing and Information Systems
The timetabling problem arising from a university in Indonesia is addressed in this paper.It involves the assignment of teachers to the courses and course sections. We formulate theproblem as a mathematical programming model. Two different algorithms, mainly basedon simulated annealing (SA) and tabu search (TS) algorithms, are proposed for solving theproblem. The proposed algorithms consist of two phases. The first phase involves allocatingthe teachers to the courses and determining the number of courses to be assigned to eachteacher. The second phase involves assigning the teachers to the course sections in order tobalance the teachers’ load. The performance of the proposed …
Solving The Quadratic Assignment Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh
Solving The Quadratic Assignment Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh
Research Collection School Of Computing and Information Systems
This paper presents a hybrid algorithm to solve the Quadratic Assignment Problem (QAP). The proposed algorithminvolves using the Greedy Randomized Adaptive Search Procedure (GRASP) to obtain an initial solution, and then using a combinedSimulated Annealing (SA) and Tabu Search (TS) algorithm to improve the solution. Experimental results indicate that the hybridalgorithm is able to obtain good quality solutions for QAPLIB test problems within reasonable computation time.