Spatial transcriptomics has revolutionized the ability to investigate transcriptional patterns within tissue morphology. However, many ST clustering pipelines operate on a single preselected gene set, typically prioritizing either highly variable genes (HVGs) or spatially variable genes (SVGs), and therefore may not directly model how genes with different levels of global variability provide complementary cues for spatial domain identification. Although non-HVG signals can be partially captured through SVG selection and spatial graph modeling, a dedicated two-view formulation that disentangles high-variance and low-variance gene subsets and fuses them under a unified objective remains underexplored. To this end, we propose a Spatial Transcriptomics clustering framework for Cross-view information Fusion, termed STCF, which casts HVGs and low-variability genes (LVGs) as two gene-expression views and integrates them via a plug-and-play cross-view fusion strategy. Specifically, STCF introduces a cross-view fusion mechanism that employs reverse-scaled cosine error loss (R-SCE) to balance alignment and separation of gene embeddings, ensuring robust representation learning while preserving spatial coherence, which enhances the model's ability to resolve fine-grained spatial structures. Extensive experiments on three benchmark datasets (DLPFC, HBC, and MBA) demonstrate the superiority, effectiveness, and transferability of STCF. Case studies further validate its ability to uncover latent spatial patterns and improve clustering precision.

Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces theUR4NNVverification framework, which utilizes under-approximation reachability analysis for DNN verification for the first timeUR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNVunder-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach,UR4NNVeffectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency ofUR4NNVsignificantly reducing the impact of the "unknown dilemma".

Spatial transcriptomics technologies enable the integration of gene expression profiles with spatial context, facilitating a deeper understanding of tissue architecture through downstream tasks such as clustering. However, existing approaches predominantly focus on highly variable genes (HVGs), while the informative structural and contextual signals embedded in low variability genes (LVGs) remain largely underutilized. To bridge this gap, we propose SALVG (Spatial Augmentation via Latent Variable Genes), a novel and plug-and-play framework that leverages LVG-derived structural priors to enhance HVG representation learning for spatial clustering. Specifically, SALVG constructs spatial, feature, and combined graphs for both HVGs and LVGs, and introduces two graph-based augmentation strategies to inject LVG information into HVG graphs. The first strategy enhances the HVG combined graph directly using the LVG combined graph, while the other individually augments HVG spatial and feature graphs with their LVG counterparts before fusing them into a new combined representation. These enhanced graph structures are subsequently employed for downstream clustering. To the best of our knowledge, SALVG is the first framework to exploit LVG signals for assisting HVG-centric spatial transcriptomics clustering, effectively capturing complementary structural and contextual cues. Experiments on multiple benchmarks demonstrate its effectiveness, robustness, and transferability. Case studies further confirm that LVG-derived structure enhances biological interpretability by revealing coherent spatial and cellular patterns.

Spatial transcriptomics (ST) technologies provide gene expression measurements with spatial resolution, enabling the dissection of tissue structure and function. A fundamental challenge in ST analysis is clustering spatial spots into coherent functional regions. While existing models effectively integrate expression and spatial signals, they largely overlook sequence-level biological priors encoded in the DNA sequences of expressed genes. To bridge this gap, we propose SAINT (Sequence-Aware Integration for Nucleotide-informed Transcriptomics), a unified framework that augments spatial representation learning with nucleotide-derived features. We construct sequence-augmented datasets across 14 tissue sections from three widely used ST benchmarks (DLPFC, HBC, and MBA), retrieving reference DNA sequences for each expressed gene and encoding them using a pretrained Nucleotide Transformer. For each spot, gene-level embeddings are aggregated via expression-weighted and attention-based pooling, then fused with spatial-expression representations through a late fusion module. Extensive experiments demonstrate that SAINT consistently improves clustering performance across multiple datasets. Experiments validate the superiority, effectiveness, sensitivity, and transferability of our framework, confirming the complementary value of incorporating sequence-level priors into spatial transcriptomics clustering.

Neural networks are important computational models used in the domains of artificial intelligence and software engineering. Parameters of a neural network are obtained via training it against a specific dataset with a standard process, which guarantees each sample within that set is mapped to the correct class. In general, for a trained neural network, there is no warranty of high-level properties, such as fairness, robustness, and so forth. In this case, one need to tune the parameters in an alternative manner, and it is called repairing. In this paper, we present AutoRIC ( Auto mated R epair w I th C onstraints), an analytical-approach-based white-box repairing framework against general properties that could be quantitatively measured. Our approach is mainly based on constrained optimization, namely, we treat the properties of neural network as the optimized objective described by a quadratic formula about the faulty parameters. To ensure the classification accuracy of the repaired neural network, we impose linear inequality constraints to the inputs that obtain incorrect outputs from the neural network. In general, this may generate a huge amount of constraints, resulting in the prohibitively high cost in the problem solving, or even making the problem unable to be solved by the constraint solver. To circumvent this, we present a selection strategy to diminish the restrictions, i.e., we always select the most ‘strict’ ones into the constraint set each time. Experimental results show that repairing with constraints performs efficiently and effectively. AutoRIC tends to achieve a satisfactory repairing result whereas brings in a negligible accuracy drop. AutoRIC enjoys a notable time advantage and this advantage becomes increasingly evident as the network complexity rises. Moreover, experiment results also demonstrate that repairing based on unconstrained optimizations are not stable, which embodies the necessity of constraints.

Deep neural network (DNN) has been increasingly deployed as a key component in safety-critical systems. However, the credibility of DNN components is uncertain due to the absence of formal specifications for their data preconditions, which are essential for ensuring trustworthy postconditions.In this paper, we propose a guess-and-check-based framework PreBoxes to automatically synthesize Boxes sufficient preconditions for DNN concerning rich safety and robustness postconditions.The framework operates in two phases: the guess phase generates potentially complex candidate preconditions through heuristic methods, while the check phase verifies these candidates with formal guarantees.The entire framework supports automatic and adaptive iterative running to obtain weaker preconditions as well.Such resulting preconditions can be leveraged to shield DNN for safety and enhance the interpretability of DNN in application.PreBoxes has been evaluated on over 20 models with 23 trustworthy properties of 4 benchmarks and compared with 3 existing typical schemes.The results show that not only does PreBoxes generally infer weaker non-trivial sufficient preconditions for DNN than others, but also it expands competitive capabilities to handle both complex properties and Non-ReLU complex structured networks.

Recent research has revealed that deep generative models including flow-based models and Variational Autoencoders may assign higher likelihoods to out-of-distribution (OOD) data than in-distribution (ID) data. However, we cannot sample OOD data from the model. This counterintuitive phenomenon has not been satisfactorily explained and brings obstacles to OOD detection with flow-based models. In this article, we prove theorems to investigate the Kullback-Leibler divergence in flow-based model and give two explanations for the above phenomenon. Based on our theoretical analysis, we propose a new method KLODS to leverage KL divergence and local pixel dependence of representations to perform anomaly detection. Experimental results on prevalent benchmarks demonstrate the effectiveness and robustness of our method. For group anomaly detection, our method achieves 98.1% AUROC on average with a small batch size of 5. On the contrary, the baseline typicality test-based method only achieves 64.6% AUROC on average due to its failure on challenging problems. Our method also outperforms the state-of-the-art method by 9.1% AUROC. For point-wise anomaly detection, our method achieves 90.7% AUROC on average and outperforms the baseline by 5.2% AUROC. Besides, our method has the least notable failures and is the most robust one.

Recently, the interpretability and verification of deep learning have attracted enormous attention from both academic and industrial communities, aiming to gain users’ trust and ease their concerns. To guide learning procedures or data operations carried out in a more interpretable way, in this paper, we put a similar perspective on image datasets, the inputs of deep learning. Based on manifold learning, we work out an interpretable geometrical characterization on the curvity of manifolds to depict the feature density of datasets, which is represented with the ratio of the Euclidean distance and the geodesic distance. It is a noteworthy characteristic of image datasets and we take the dataset compression and enhancement problems as application instances via sample credit assignment with the geometrical information. Experiments on typical image datasets have justified the effectiveness and enormous prospect of the presented geometrical characteristic.

Kullback-Leibler (KL) divergence is one of the most important measures to calculate the difference between probability distributions. In this paper, we theoretically study several properties of KL divergence between multivariate Gaussian distributions. Firstly, for any two $n$-dimensional Gaussian distributions $\mathcal{N}_1$ and $\mathcal{N}_2$, we prove that when $KL(\mathcal{N}_2||\mathcal{N}_1)\leq \varepsilon\ (\varepsilon>0)$ the supremum of $KL(\mathcal{N}_1||\mathcal{N}_2)$ is $(1/2)\left((-W_{0}(-e^{-(1+2\varepsilon)}))^{-1}+\log(-W_{0}(-e^{-(1+2\varepsilon)})) -1 \right)$, where $W_0$ is the principal branch of Lambert $W$ function. For small $\varepsilon$, the supremum is $\varepsilon + 2\varepsilon^{1.5} + O(\varepsilon^2)$. This quantifies the approximate symmetry of small KL divergence between Gaussian distributions. We further derive the infimum of $KL(\mathcal{N}_1||\mathcal{N}_2)$ when $KL(\mathcal{N}_2||\mathcal{N}_1)\geq M\ (M>0)$. We give the conditions when the supremum and infimum can be attained. Secondly, for any three $n$-dimensional Gaussian distributions $\mathcal{N}_1$, $\mathcal{N}_2$, and $\mathcal{N}_3$, we theoretically show that an upper bound of $KL(\mathcal{N}_1||\mathcal{N}_3)$ is $3\varepsilon_1+3\varepsilon_2+2\sqrt{\varepsilon_1\varepsilon_2}+o(\varepsilon_1)+o(\varepsilon_2)$ when $KL(\mathcal{N}_1||\mathcal{N}_2)\leq \varepsilon_1$ and $KL(\mathcal{N}_2||\mathcal{N}_3)\leq \varepsilon_2$ ($\varepsilon_1,\varepsilon_2\ge 0$). This reveals that KL divergence between Gaussian distributions follows a relaxed triangle inequality. Note that, all these bounds in the theorems presented in this work are independent of the dimension $n$. Finally, we discuss several applications of our theories in deep learning, reinforcement learning, and sample complexity research.

Robustness of deep neural networks (DNNs) has caused great concerns in the academic and industrial communities, especially in safety-critical domains. Instead of verifying whether the robustness property holds or not in certain neural networks, this paper focuses on training robust neural networks with respect to given perturbations. State-of-the-art training methods, interval bound propagation (IBP) and CROWN-IBP, perform well with respect to small perturbations, but their performance declines significantly in large perturbation cases, which is termed “drawdown risk” in this paper. Specifically, drawdown risk refers to the phenomenon that IBP-family training methods cannot provide expected robust neural networks in larger perturbation cases, as in smaller perturbation cases. To alleviate the unexpected drawdown risk, we propose a global and monotonically decreasing robustness training strategy that takes multiple perturbations into account during each training epoch (global robustness training), and the corresponding robustness losses are combined with monotonically decreasing weights (monotonically decreasing robustness training). With experimental demonstrations, our presented strategy maintains performance on small perturbations and the drawdown risk on large perturbations is alleviated to a great extent. It is also noteworthy that our training method achieves higher model accuracy than the original training methods, which means that our presented training strategy gives more balanced consideration to robustness and accuracy.

Abstract Secure multi-party computation (MPC) is a promising technique for privacy-persevering applications. A number of MPC frameworks have been proposed to reduce the burden of designing customized protocols, allowing non-experts to quickly develop and deploy MPC applications. To improve performance, recent MPC frameworks allow users to declare variables secret only for these which are to be protected. However, in practice, it is usually highly non-trivial for non-experts to specify secret variables: declaring too many degrades the performance while declaring too less compromises privacy. To address this problem, in this work we propose an automated security policy synthesis approach to declare as few secret variables as possible but without compromising security. Our approach is a synergistic integration of type inference and symbolic reasoning. The former is able to quickly infer a sound—but sometimes conservative—security policy, whereas the latter allows to identify secret variables in a security policy that can be declassified in a precise manner. Moreover, the results from symbolic reasoning are fed back to type inference to refine the security types even further. We implement our approach in a new tool PoS4MPC. Experimental results on five typical MPC applications confirm the efficacy of our approach.

In this work-in-progress innovative practice paper, we argue the application-ability training in Discrete Mathematics (DM) should be enhanced for students majoring in computing science. Our motivation is based on the analysis of the differences in learning outcomes between DM and other branches of Math courses, the special role of DM in computer science (CS) courses and the gaps between DM and other CS courses. Motivated by the above analysis, we rethink of CS undergraduate education program as a DM-centric program. Furthermore, we make an experimental implementation of the DM-centric program and enhance application-ability training by designing and adopting many large-scale projects from various related topics, such as database, satisfiability, deductive proof and so on. Each project is decomposed into several sub-projects, which are integrated with a project-based learning environment. The large-scale projects derived from related CS courses enable students to get in touch with various computing topics related to DM applications at an early stage in the learning process. The learning environment with the ability of automatic assessment enables students to complete the projects in a step-by-step manner. The preliminary feedback from 219 students after taking the redesigned DM course shows the promising effects on students' following learning.

The increasing control complexity of Noisy Intermediate-Scale Quantum (NISQ) systems underlines the necessity of integrating quantum hardware with quantum software. While mapping heterogeneous quantum-classical computing (HQCC) algorithms to NISQ hardware for execution, we observed a few dissatisfactions in quantum programming languages (QPLs), including difficult mapping to hardware, limited expressiveness, and counter-intuitive code. In addition, noisy qubits require repeatedly performed quantum experiments, which explicitly operate low-level configurations, such as pulses and timing of operations. This requirement is beyond the scope or capability of most existing QPLs. We summarize three execution models to depict the quantum-classical interaction of existing QPLs. Based on the refined HQCC model, we propose the Quingo framework to integrate and manage quantum-classical software and hardware to provide the programmability over HQCC applications and map them to NISQ hardware. We propose a six-phase quantum program life-cycle model matching the refined HQCC model, which is implemented by a runtime system. We also propose the Quingo programming language, an external domain-specific language highlighting timer-based timing control and opaque operation definition, which can be used to describe quantum experiments. We believe the Quingo framework could contribute to the clarification of key techniques in the design of future HQCC systems.

The reactive system synthesis for GR(1) fragment of LTL has been widely studied and used in different works. Meanwhile, automatic procedures for generating distributed systems from global behaviors are also thoroughly studied. In this paper, we present a method that automatically constructs cooperative controllers for multi-robot systems from global tasks specified by GR(1). We combine reactive systems synthesis and distributed systems synthesis to solve global task planning problems for multi-robot systems. In short, we specify global tasks for a multi-robot system which consists of several robots, then our algorithm generates individual controllers for robots and also synthesizes a communication strategy. The communication strategy makes robots as a cooperative system through synchronizing them on environment inputs and finally achieves the goal of completing the global tasks. This paper can be used as a cooperative framework for multi-robot systems.

Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons, e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications over a given signature. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model and over a given signature. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting. Furthermore, we analyse the computational complexity of some basic reasoning tasks for the fragment CTLAF in particular.

In real-world environments, robotic task planning is expected to handle both partial observability and unexpected dynamics of the environment. A robust plan for the task requires the robot's observation actions to concurrently run with the task actions, to observe and adapt to environmental changes. The Partially Observable Markov Decision Process (POMDP) has been widely applied for planning under partially observable domains. For realistic robotic tasks, however, the POMDP model and planning algorithm are quite restrictive and unrealistic. One limitation is that task actions are modelled as atomic entities that only have endpoint effects, with no conditions specified at arbitrary points during task action execution. Also, the observation is obtained only after each task action execution, with no intermediate observations and decision-making during task action execution. To mitigate the limitations of POMDP planning, this paper first proposes an Adjoint Action Model (AAM) that explicitly defines the continuous interaction between robot's observation and task actions. Then we extend the POMDP task action model with intermediate invariant conditions which specifies the runtime properties of action execution. Finally, we propose the AAM-extended POMDP planning approach which handles observation action planning and task replanning for task action execution. We experimentally demonstrate that the plan from our proposed approach is more effective and robust to cope with the environment dynamics, comparing with the standard POMDP planning approach.

The synthesis problem is to construct a system fulfilling some specific requirements when interacting with the environment, which is one of the most crucial and challenging tasks in robotics. In comparison to the case of dealing with a single robot, synthesizing of a system constituted with multiple robots is, in general, much more involved. Actually, information is shared among robots in the latter case, and for a fixed robot, when fictively merging the rest ones into its environment, we are confronted with imperfect description of environments. In this article, we present an iterative controller synthesis approach to dealing with multirobot systems. In our model, the behaviors and outputs of one robot can be observed by the other ones, as a part of their inputs. To make our model more flexible, we allow the mechanism of “partial observation,” namely, only a part of outputs can be observed by other robots on some particular sensors. Our synthesis approach is conductive in an iterative manner. By analyzing the dependence among robots, we first try to synthesize controllers for some of them and then extract a set of invariants from the solved part to refine other ones. Repeatedly and iteratively using this way, we may arrive at a complete solution. Meanwhile, in comparison to the monolithic approach, using the iterative manner usually produces a much more compact result, which means that the size of the controller is smaller.

Bounded model checking is among the most efficient techniques for the automated verification of concurrent programs. However, due to the nondeterministic thread interleavings, a large and complex formula is usually required to give an exact encoding of all possible behaviors, which significantly limits the scalability. Observing that the large formula is usually dominated by the exact encoding of the scheduling constraint, this paper proposes a novel scheduling constraint based abstraction refinement method for multi-threaded C program verification. Our method is both efficient in practice and complete in theory, which is challenging for existing techniques. To achieve this, we first proposed an effective and powerful technique which works well for nearly all benchmarks we evaluated. We have proposed the notion of Event Order Graph (EOG), and have devised two graph-based algorithms over EOG for counterexample validation and refinement generation, which can often obtain a small yet effective refinement constraint. Then, to ensure completeness, our method was enhanced with two constraint-based algorithms for counterexample validation and refinement generation. Experimental results on SV-COMP 2017 benchmarks and two real-world server systems indicate that our method is promising and significantly outperforms the state-of-the-art tools.

Program verification is one of the most important methods to ensuring the correctness of concurrent programs. However, due to the path explosion problem, concurrent program verification is usually time consuming, which hinders its scalability to industrial programs. Parallel processing is a mainstream technique to deal with those problems which require mass computing. Hence, designing parallel algorithms to improve the performance of concurrent program verification is highly desired. This paper focuses on parallelization of the abstraction refinement technique, one of the most efficient techniques for concurrent program verification. We present a parallel refinement framework which employs multiple engines to refine the abstraction in parallel. Different from existing work which parallelizes the search process, our method achieves the effect of parallelization by refinement constraint and learnt clause sharing, so that the number of required iterations can be significantly reduced. We have implemented this framework on the scheduling constraint based abstraction refinement method, one of the best methods for concurrent program verification. Experiments on SV-COMP 2018 show the encouraging results of our method. For those complex programs requiring a large number of iterations, our method can obtain a linear reduction of the iteration number and significantly improve the verification performance.

Scheduling constraint based abstraction refinement (SCAR) is one of the most efficient methods for verifying programs under sequential consistency (SC). However, most multi-processor architectures implement weak memory models (WMMs) in order to improve the performance of a program. Due to the nondeterministic execution of those memory operations by the same thread, the behavior of a program under WMMs is much more complex than that under SC, which significantly increases the verification complexity. This paper elegantly extends the SCAR method to WMMs such as TSO and PSO. To capture the order requirements of an abstraction counterexample under WMMs, we have enriched the event order graph (EOG) of a counterexample such that it is competent for both SC and WMMs. We have also proposed a unified EOG generation method which can always obtain a minimal EOG efficiently. Experimental results on a large set of multi-threaded C programs show promising results of our method. It significantly outperforms state-of-the-art tools, and the time and memory it required to verify a program under TSO and PSO are roughly comparable to that under SC.

This paper presents the Y ogar - CBMC tool for verification of multi-threaded C programs. It employs a scheduling constraint based abstraction refinement method for bounded model checking of concurrent programs. To obtain effective refinement constraints, we have proposed the notion of Event Order Graph (EOG) , and have devised two graph-based algorithms over EOG for counterexample validation and refinement generation. The experiments in SV-COMP 2017 show the promising results of our tool.

Runtime verification is a dynamic verification technique widely used in practice. In this paper we revisit the runtime verification technique with formula progression, which verifies the execution trace step by step by progressing the desired property written in temporal logic. The previous work did not discuss explicitly the bound for the sizes of expanded formulas, while the successive invoking of formula progression is likely to cause divergence. In this paper, we present the convergent formula progression by introducing a novel fix-point reduction technique, and prove it guarantees the sizes of expanded formulas be always convergent. To the best of our knowledge, this is the first work discussing the convergence of formula progression. Furthermore, we implement the new runtime verification framework, and experiments show the efficiency of our proposed strategy.

Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.

The growing design-productivity gap has made designers shift toward using high-level synthesis (HLS) techniques to generate register transfer level design from high-level languages. Unfortunately, this translation process is very complex and may introduce bugs into the generated design, which can create a mismatch between what a designer intends and what is actually implemented in the circuit. In this paper, we present an equivalence checking method to validate the result of HLS scheduling against the initial high-level program. Finite state machine with data path (FSMD) models were used to represent designs before and after scheduling. The proposed method uses a bisimulation relation approach to prove equivalence. The automatically established bisimulation relation guarantees that for each execution sequence in the design before scheduling, a related and equivalent execution sequence exists in the design after scheduling and vice versa. Our method provides a unified way to deal with various scheduling optimizations. We have implemented our validation technique and compared it with a state-of-the-art HLS scheduling verification method. The promising results show the effectiveness and efficiency of our method.

In this poster, we report our experience in teaching introductory courses on programming based on program derivation using formal method. Based on an ongoing teaching activity, we present some preliminary results on the students' experiences.

Subsequently to the wall of performance and power consumption, the dependability of computing, caused by soft errors, has become a growing design concern. Since Register Files (RFs) are accessed very frequently and cannot be well protected, soft errors occurred in them is one of the top reasons for affecting the reliability of programs. To access the soft errors vulnerability of RFs, this paper presents a static estimating method via interprocedural data flow analysis. Adopting a previous method, the vulnerability of a register is firstly decomposed into intrinsic and conditional basic block vulnerabilities. Under the prerequisite of context sensitivity, we focus on the computation the post conditions of basic blocks, which can be viewed as the living probability of the target register in the future usage. Finally, the program reliability can be calculated quantitatively under the occurrence of soft errors in RFs. Experimental results from the MiBench benchmarks indicate that our method is more accurate, and compatible with the AVF methods. We also reveal that the reliability of a program has a connection with its structure, such as the RVF factors, which suggests adopting the application specified protected mechanisms for tolerating soft errors occurred in RFs.

PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper, we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover, we show how to implement this algorithm via the BDD based symbolic approach.