9 citations · 51 across the 16 of their papers we have counts for
16 papers
FREPA: An Automated and Formal Approach to Requirement Modeling and Analysis in Aircraft Control Domain
Jincao Feng, Weikai Miao, Hanyue Zheng +8
Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The indus…
Identifying Boundary Conditions with the Syntax and Semantic Information of Goals
Yechuan Xia, Jianwen Li, Shengping Xiao +2
In goal-oriented requirement engineering, boundary conditions(BC) are used to capture the divergence of goals, i.e., goals cannot be satisfied as a whole in some circumstances. As…
Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning
Peng Jin, Min Zhang, Jianwen Li +2
Formally verifying Deep Reinforcement Learning (DRL) systems is a challenging task due to the dynamic continuity of system behaviors and the black-box feature of embedded neural ne…
FakePolisher: Making DeepFakes More Detection-Evasive by Shallow Reconstruction
Yihao Huang, Felix Juefei-Xu, Run Wang +7
At this moment, GAN-based image generation methods are still imperfect, whose upsampling design has limitations in leaving some certain artifact patterns in the synthesized image.…
FakeLocator: Robust Localization of GAN-Based Face Manipulations
Yihao Huang, Felix Juefei-Xu, Qing Guo +2
Full face synthesis and partial face manipulation by virtue of the generative adversarial networks (GANs) and its variants have raised wide public concerns. In the multi-media fore…
SAT-based Explicit LTLf Satisfiability Checking
Jianwen Li, Kristin Y. Rozier, Geguang Pu +2
We present here a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transiti…
A Symbolic Approach to Safety LTL Synthesis
Shufang Zhu, Lucas M. Tabajara, Jianwen Li +2
Temporal synthesis is the automated design of a system that interacts with an environment, using the declarative specification of the system's behavior. A popular language for prov…
Symbolic LTLf Synthesis
Shufang Zhu, Lucas M. Tabajara, Jianwen Li +2
LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to…
Safety Model Checking with Complementary Approximations
Jianwen Li, Shufang Zhu, Yueling Zhang +2
Formal verification techniques such as model checking, are becoming popular in hardware design. SAT-based model checking techniques such as IC3/PDR, have gained a significant succe…
SAT-based Explicit LTL Reasoning
Jianwen Li, Shufang Zhu, Geguang Pu +1
We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of th…
LTLf satisfiability checking
Jianwen Li, Lijun Zhang, Geguang Pu +2
We consider here Linear Temporal Logic (LTL) formulas interpreted over \emph{finite} traces. We denote this logic by LTLf. The existing approach for LTLf satisfiability checking is…
Fast LTL Satisfiability Checking by SAT Solvers
Jianwen Li, Geguang Pu, Lijun Zhang +2
Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of…
Polsat: A Portfolio LTL Satisfiability Solver
Jianwen Li, Geguang Pu, Lijun Zhang +3
In this paper we present a portfolio LTL-satisfiability solver, called Polsat. To achieve fast satisfiability checking for LTL formulas, the tool integrates four representative LTL…
MDM: A Mode Diagram Modeling Framework
Zheng Wang, Geguang Pu, Jianwen Li +5
Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observe…
On the Relationship between LTL Normal Forms and Buechi Automata
Jianwen Li, Geguang Pu, Lijun Zhang +3
In this paper, we consider the problem of translating LTL formulas to Buechi automata. We first translate the given LTL formula into a special disjuctive-normal form (DNF). The for…
MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
Zheng Wang, Geguang Pu, Shenchao Qin +5
Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observe…