Zili Wang.

This work presents an integrated ecosystem for eliciting and validating Mission-time Linear Temporal Logic specifications. It brings complementary tools and workflows together so that users can move from informal requirements to formal specifications and check that those specifications capture the intended behavior.

WEST is an interactive tool for validating MLTL specifications by visualizing the traces that satisfy a formula. The paper presents its command-line and graphical interfaces, five independent methods used to validate the implementation, and scalability results over several suites of randomly generated formulas.

This work formalizes MLTL syntax, semantics, and formula progression in Isabelle/HOL. It proves the progression algorithm correct, resolves errors and missing assumptions in prior presentations, and exports executable code that can support trustworthy formula evaluation and benchmark generation.

This paper gives an algorithm that partitions the language of an MLTL formula into disjoint sublanguages represented by related formulas. The algorithm and its correctness proof are mechanized in Isabelle/HOL, exported to executable code, and evaluated experimentally.

This work mechanizes the WEST transformation from MLTL formulas to trace regular expressions and proves semantic equivalence in Isabelle/HOL. It also develops verified support for restricted regular-expression equivalence and uses exported code to validate the existing WEST implementation.

This paper studies responsible-AI considerations for air traffic management and applies a practical subset of them to a runway-configuration assistance tool. It examines how an AI decision-support system can be assessed and communicated in a safety-conscious operational setting.

Convolutional neural networks trained only on recordings of individual words spontaneously generate outputs containing two or three concatenated words. The study reproduces this behavior across models and datasets, finds novel word combinations, and discusses its implications for compositionality and models of syntax emerging directly from speech.

TreeVada makes black-box context-free grammar inference deterministic by pre-structuring sample programs according to common nesting rules and recursively applying learned rules. In experiments it runs faster and infers higher-quality grammars than the prior nondeterministic Arvada approach.

This paper characterizes the computations satisfying an MLTL formula using trace regular expressions and proves the construction sound and complete. It introduces an automated validation algorithm, studies its complexity, and evaluates an open-source implementation with a generated test suite and graphical interface.

This paper continues the classification of permutation groups by the number of orbits induced on a power set. It improves earlier theory and GAP algorithms to classify groups with n + r set-orbits for the previously unresolved range 16 through 33.

The paper studies character codegrees as invariants of finite groups. It proves that the codegree sets of selected non-abelian simple groups, including PSL(3,3), determine those groups up to isomorphism.

A permutation group acting on a finite set also acts on its power set, producing a number of set orbits that is useful in bounding conjugacy classes. This paper determines the optimal ratio between the logarithms of the number of set orbits and the group order when large alternating composition factors are excluded.