====== Explainable Behavioral Engineering (NCN Opus 31/ST6) ====== ===== Research Vision ===== This research programme investigates how behavioral models, formal logic, automated reasoning, and explainable diagnostics can support the analysis, verification, and understanding of software systems developed with AI assistance. The long-term objective is to establish foundations for **Explainable Behavioral Engineering (EBE)**, enabling the transformation of requirements and behavioral artifacts into formally analyzable representations supporting verification, diagnosis, and explainability. Requirements ↓ Behavioral Models ↓ Logical Specifications ↓ Verification ↓ Diagnostic Explainability ↓ Behavioral Accountability ===== Level 1: Published Foundations ===== This level contains peer-reviewed results forming the published scientific foundation of the programme. ([Kli 25 FSE-AI-IDE], [Kli Sem 25 EASE], [Kli Wit 25 EMSE], [Kli 25 PACIS], [Kli 24 IS], [Kli Wit 24 ASE-RENE], [Kli 24 ASE-ASYDE], [Kli 24 ISD], [Kli 23 ISD], [Kli 19 LAMP], [Kli 18 Access], [Kli 14 AMCS].) The complete publication record underpinning these foundations is available in the author's publication profile and in the project proposal and is therefore not reproduced on this page. The published foundations establish the feasibility of: * transforming behavioral models into logical specifications, * applying automated reasoning and theorem proving, * integrating behavioral modeling with software engineering workflows, * supporting AI-assisted software engineering through formal methods. ===== Level 2: Ongoing Research (=articles under review) ===== This level documents current research directions extending the published foundations toward a coherent programme of explainable and verifiable behavioral engineering. **Behavioral Modeling and Elicitation** [Kli 26d] Radoslaw Klimek "AI-Assisted Behavioural Modelling from Logical Squares". Title changed to "Reasoning Scaffolds for AI-Assisted Behavioural Modelling: A Logical-Square Instantiation". Available: https://drive.google.com/file/d/1NfuY7yZas993QiVlwNq-sPOXHCtUF-h5/view?usp=sharing. **ACCEPTED** Conference paper, MODELS 2026 (Rank A, 140 MNiSW points). Acceptance notification: https://drive.google.com/file/d/1ZCM-jHR01vMIH-sOkXksY8ikYh4AcmxU/view?usp=drive_link. List of accepted papers: https://conf.researchr.org/track/models-2026/models-2026-nier#event-overview **Behavioral Verification** [Kli Wit 25 EMSE] Radosław Klimek, Julia Witek “Logic Mining from Process Logs: Towards Automated Specification and Verification”. Pre-print version available at https://arxiv.org/abs/2506.08628 The extended version of the conference paper has been submitted to the JCR journal with Q2 quartiles, 140 MNiSW points, under review. [Kli et at 26] Natania Dyczek, Jagoda Flejmer, Radoslaw Klimek "Why Formal Constraints Fail on Real-World Execution Logs: The Dead-End Phenomenon". Title changed to "Dead-End Ratio: A Behavioral Model Quality Metric for Constraint-Aware Runtime Verification". Available at: https://drive.google.com/file/d/1ZaSoLkqn521gbJKhuSs_rruhXlYtDe2A/view?usp=sharing. **ACCEPTED** Warokshop paper at ASE 2026 (ASE is a flagship conference Core Rank A*, 200 MNiSW points). **Diagnostic Explainability** [Kli Bla 26] Radosław Klimek, Jakub Blazowski “Towards Diagnostic Explainability inWorkflow Verification via Shapley Attribution”. Available at: https://drive.google.com/file/d/1AtZUpwG9lA3X074wgk1LmCLyrRPdi-ih/view?usp=drive_link. **ACCEPTED** Conference paper, ASE 2026 (Flagship conference Core Rank A*, 200 MNiSW points). Acceptance notification: https://drive.google.com/file/d/1jR-GT5LYMa7f6Vnon_D183MkQAcbwfih/view?usp=drive_link. See conference program: https://conf.researchr.org/track/ase-2026/ase-2026-nier [Kli 26f] Radoslaw Klimek „Prompt-to-Feature Attribution for Explainable LLM-Based Software Generation”. Available at: https://drive.google.com/file/d/1erB_Iz6Kcymm10nw3Lb4TPwN-n1G7jPY/view?usp=sharing. **ACCEPTED** Workshop paper at ASE 2026 (ASE is a flagship conference Core Rank A*, 200 MNiSW points). [Kli 26] Radoslaw Klimek "Toward Defensible System Behavior in AI-Assisted Software Engineering". Title changed to "Toward Defensible System Behavior for AI-Generated Software Artifacts" Available at: https://drive.google.com/file/d/1WEZGiLEQTk2CVMqgtl0_vYGFaX0pkhX-/view?usp=sharing. **ACCEPTED** Workshop paper at ASE 2026, (ASE is a flagship conference, Rank A*, 200 pkt pkt MNiSW). List of accepted papers: https://conf.researchr.org/home/ase-2026/rase-2026#event-overview [Klo Kli 26] Michał Klos, Radoslaw Klimek "Learning System Behavior from Logs: Graph-Based Anomaly Detection Using Attribute-Aware Autoencoders". Available at: https://drive.google.com/file/d/1FEitqDCgZxdCjjI4pXMdOEoLzQSU2cMQ/view?usp=sharing. Conference paper, Rank A, 140 pkt pkt MNiSW, under review. **AI-Assisted Software Engineering** [Kli 26b] Radoslaw Klimek "What Fails in Empirical SE and AI4SE? A Study of Evaluation Fragility". Available at: https://drive.google.com/file/d/128JSq_4HOYNfb4QZc_73Q9TJfbSf8vfk/view?usp=drive_link (and also https://drive.google.com/file/d/1UBC-9oOMX1ga7pfL6l9g3mObFpqD1ezy/view?usp=drive_link). **ACCEPTED** Conference paper, ICSEM 2026 (Conference Core Rank A, 140 MNiSW points). Acceptance notification: https://drive.google.com/file/d/11Nxa5CnOSNd5-mEoSNcwEVLHqBwDGWhd/view?usp=drive_link. See conference program: https://conf.researchr.org/track/icsme-2026/icsme-2026-replication-and-negative-results?#event-overview. [Kli 26c] Radoslaw Klimek "A Workflow-Based LLM Assistant for Iterative and Verified Requirements Engineering". Title changed to: "A Workflow-Driven Multi-Agent Architecture for Requirements Engineering". Available at: https://drive.google.com/file/d/1B_g15sM43HLliKHjzsyioi1HL0dYRXx4/view?usp=sharing. **ACCEPTED** Workshop paper at ASE 2026, (ASE is a flagship conference, Rank A*, 200 pkt pkt MNiSW). **Others / Adjacent Research** [Kli 26e] Radoslaw Klimek "Context-Aware Orchestration of Adaptive Decisions in Intelligent Environments". Available at: https://drive.google.com/file/d/1RHOAYRuJ_aKXy0ZWlQIhk41u0z7dmdqh/view?usp=drive_link. Journal JCR/IF paper, Q1 quartile, 200 pkt, under review. [Kli Ole 26] Radoslaw Klimek, Arkadiusz Olesek "A prole-based framework for the generation of synthetic tourist mobility trajectories in urban decision support". Available at: https://drive.google.com/file/d/1l38kJN7Pv5zo2MUTrMkW2A6Ca5P7wuWU/view?usp=drive_link. Journal JCR/IF paper, Q1 quartile, 200 pkt, under review. ===== Level 3: Experimental Platforms and Research Infrastructure (future publications and ongoing developments) ===== This level contains experimental environments, benchmarks, datasets, and prototypes used to validate research hypotheses and demonstrate technical feasibility. This level comprises experimental environments, benchmark collections, datasets, and prototype systems developed to validate research hypotheses and demonstrate the technical feasibility of the proposed methods. **LOGIMINE** LOGIMINE ('''Log'''ic '''Mine'''ing and Verification Environment) is a research platform implementing the concept of '''Logic Mining''', an approach that combines process mining, formal methods, automated theorem proving, and AI-assisted software engineering within a unified behavioral reasoning environment. The central idea is to transform process execution data into formal logical representations that can be automatically analyzed, verified, compared, and explained using mature reasoning technologies. Unlike traditional process mining systems, which typically stop after discovering a behavioral model, LOGIMINE continues the analysis by automatically generating formal logical specifications and submitting them to automated theorem provers. Consequently, behavioral models become executable logical objects that support rigorous reasoning about process properties, correctness, consistency, robustness, and semantic relationships between independently discovered models. The platform provides a complete transformation pipeline starting from standard event logs (XES or CSV). Event logs are analyzed using state-of-the-art process mining techniques to discover process trees representing the observed behavior. These trees are automatically translated into workflow expressions and subsequently transformed into first-order logical specifications using the compositional Pattern-Composition (PC) algorithm. The resulting specifications are converted into the TPTP standard and verified using automated theorem provers, including Vampire and E-Prover. **Main Capabilities** LOGIMINE integrates a broad spectrum of research and engineering functionalities within a single environment. * '''Process Discovery''' – automatic discovery of behavioral models from execution traces using process mining algorithms. * '''Behavioral Modeling''' – representation of discovered behavior using process trees and workflow expressions suitable for further formal analysis. * '''Logic Mining''' – automatic generation of first-order logical specifications from behavioral models through compositional logical specification generation. * '''Automated Theorem Proving''' – formal verification of generated specifications using state-of-the-art theorem provers supporting the TPTP standard. * '''Behavioral Verification''' – analysis of consistency, satisfiability, behavioral correctness, safety, and other logical properties of process models. * '''Process Comparison''' – formal comparison of independently discovered models using logical equivalence, implication, inclusion, conjunction, and other semantic relations. * '''Compliance and What-if Analysis''' – evaluation of behavioral constraints, hypothetical modifications, and alternative execution scenarios. * '''Visualization''' – graphical presentation of process trees, workflow structures, logical specifications, and verification outcomes. * '''Benchmark Management''' – execution and comparison of verification experiments on benchmark collections, including performance evaluation of multiple theorem provers. * '''Research Data Management''' – organization of generated specifications, benchmark datasets, verification artifacts, and experimental results. **AI-Assisted Behavioral Analysis** LOGIMINE extends classical process mining by incorporating Large Language Models (LLMs) into the behavioral analysis workflow. Instead of replacing formal reasoning, LLM agents complement symbolic methods by generating synthetic event logs from natural-language descriptions, constructing experimental scenarios, supporting benchmark generation, and assisting users during exploratory behavioral analysis. The platform currently supports multiple LLM providers through a unified interface, enabling comparative evaluation of different models while maintaining the same underlying formal verification pipeline. Regardless of the selected LLM, all generated behavioral artifacts are ultimately verified using symbolic reasoning rather than accepted solely on the basis of probabilistic model outputs. **Digital Twin Game** One of the most distinctive components of LOGIMINE is the '''Digital Twin Game''', an adversarial verification framework combining digital twins, automated theorem proving, and LLM agents. In this setting, an LLM-based adversary actively searches for behavioral weaknesses by generating controlled attacks against a process model discovered from execution logs. Each generated attack is translated into a formal logical problem and evaluated using automated theorem provers. Successful attacks identify behavioral vulnerabilities, whereas unsuccessful attacks demonstrate behavioral robustness. The framework additionally supports iterative self-correction by proposing model modifications and immediately re-verifying their correctness, creating a closed loop of attack, verification, repair, and validation. **System Architecture** LOGIMINE has been designed as a modular research platform consisting of interoperable components: * Core Logic Mining engine; * Process Mining and Behavioral Modeling module; * Logic Specification Generator; * Automated Theorem Proving layer; * Behavioral Verification framework; * Process Comparison module; * Interactive Web IDE; * Synthetic Event Log Generator; * Digital Twin Game; * Benchmark Manager; * Visualization and Analytics modules. The modular architecture enables independent development of individual components while preserving a common behavioral reasoning pipeline shared by all analysis modes. **Research Applications** LOGIMINE serves as an experimental infrastructure for research in Logic Mining, behavioral modeling, process mining, formal verification, automated reasoning, explainable behavioral analysis, and AI-assisted software engineering. The platform supports reproducible experimental studies, comparative evaluation of verification methods, benchmark development, and investigation of novel concepts combining symbolic reasoning with generative artificial intelligence. By integrating behavioral modeling, logical specification generation, automated theorem proving, explainable verification, and AI-assisted analysis within a single environment, LOGIMINE provides a comprehensive platform for developing trustworthy, explainable, and formally verifiable behavioral engineering methods. A central component is LOGIMINE (Logic Mining and Verification Environment), a research platform supporting the complete pipeline from event logs to formal behavioral analysis. The platform integrates workflow discovery from execution traces, behavioral modeling using workflows and process trees, automatic generation of logical specifications, formal verification through automated theorem proving, process comparison, compliance checking, what-if analysis, and visual analytics for exploring behavioral structures and verification outcomes. Further technical details are available in the accompanying documentation: [[https://drive.google.com/file/d/1eSAquVISQSJHr_S_DQOnjosV1_gJbgfa/view?usp=drive_link|LOGIMINE IDE Documentation]], [[https://drive.google.com/file/d/1rdV_XF9o2KEY3QmGiXr-tQRx1P1vFruu/view?usp=drive_link|LOGIMINE System Documentation2]], and [[https://drive.google.com/file/d/1_mrYHZpD5cEyVDpC4Y9GDG19yIC5Zs9y/view?usp=drive_link|Digital Twin Game Documentation]]. **LOFT** **LOFT (Logical Framework and Testbench)** is a research platform for systematic benchmark engineering and experimental evaluation of automated reasoning methods. The platform supports the generation, management, execution, and analysis of logical verification problems used in software engineering, formal verification, behavioral reasoning, and automated theorem proving. LOFT goes beyond conventional benchmark runners. Instead of relying exclusively on fixed collections of existing problems, it enables researchers to construct entire benchmark families with controllable structural and semantic properties. This makes it possible to investigate how particular characteristics of logical specifications influence the performance, scalability, robustness, and reliability of theorem provers, SAT/SMT solvers, and related reasoning engines. The platform supports logical problems concerning satisfiability, consistency, implication, redundancy, conflict detection, behavioral constraints, model evolution, modularity, safety and liveness properties, theorem proving, and logical relations between specifications. Generated problems are stored in the TPTP format together with metadata describing their parameters, generation seed, and benchmark configuration. **Systematic Benchmark Engineering** The central concept implemented by LOFT is **systematic benchmark engineering**. Benchmark problems are generated from parameterized templates rather than collected as unrelated individual examples. Each benchmark family isolates a selected structural or semantic factor and allows the researcher to control its intensity, scale, or distribution. This approach supports controlled experimentation. For example, a researcher can investigate how reasoning performance changes when: * the number of clauses increases; * clause lengths follow fixed, uniform, or probabilistic distributions; * the ratio between safety and liveness constraints changes; * formulas contain increasing levels of redundancy; * selected clauses are removed or modified; * logical conflicts are introduced at different depths; * implication chains become longer; * modules become increasingly coupled; * the topology of atom co-occurrence changes; * formulas move closer to the SAT/UNSAT phase-transition region. Because the benchmark parameters are explicitly recorded, experiments can be repeated using the same seed and configuration. LOFT therefore supports both exploratory experimentation and reproducible comparative studies. **Main Capabilities** LOFT integrates the following functionality within a single environment: * **Parameterized problem generation** – construction of logical benchmark families from configurable generators; * **Preset management** – use of predefined configurations such as short, medium, long, weak, strong, or domain-specific benchmark variants; * **Controlled randomization** – support for random or fixed seeds, enabling both diversity and reproducibility; * **TPTP generation** – creation of benchmark problems in the standard TPTP representation; * **Syntax checking** – optional validation of generated TPTP files before benchmark execution; * **Workspace management** – organization of problems, settings, converted files, and results into separate experimental workspaces; * **Multi-prover orchestration** – parallel execution of multiple theorem provers and solvers on selected benchmark collections; * **Format conversion** – automatic conversion of TPTP problems into formats required by individual reasoning engines; * **Result streaming** – real-time delivery of benchmark results through WebSocket communication; * **Performance measurement** – recording of real execution time, system time, peak memory use, and solver status; * **Comparative visualization** – interactive charts presenting how prover performance changes with benchmark parameters; * **Result persistence** – storage of complete benchmark reports for later inspection and comparison. **Benchmark Families** The platform currently provides eighteen principal benchmark families, including two variants of Problem 9. Together, these families cover a wide spectrum of structural, semantic, and computational properties. **Formula Size and Clause Structure** Problems P01–P06 investigate how formula size, clause length, clause distributions, atom-to-clause ratios, and safety/liveness proportions affect reasoning performance. The generated specifications may use: * fixed clause lengths; * several predefined length groups; * uniform distributions; * Poisson-based distributions; * different numbers of atoms; * controlled proportions of safety and liveness clauses. These families support systematic scalability studies and analysis of how basic syntactic properties influence execution time and memory consumption. **Logical Composition and Relations** Problem P07 studies the composition of several independently generated formulas using conjunction or disjunction. The resulting global specification is tested against additional logical requirements. Problems P08, P09a, and P09b investigate relations derived from logical squares, including contradiction, subcontrariety, and subalternation. They additionally allow researchers to study structural and semantic asymmetry between formulas of different sizes or different safety/liveness profiles. These benchmark families are particularly relevant to research on behavioral specification comparison, logical model relationships, and symbolic analysis of alternative system descriptions. **Behavioral Evolution and Redundancy** Problem P10 models the evolution of behavioral specifications. A base formula is modified by removing, adding, or replacing selected clauses, and the logical relationship between the original and modified specification is then analyzed. Problem P11 investigates controlled redundancy. Additional clauses may be exact duplicates, logically equivalent variants, or clauses related through literal inclusion. The benchmark can test whether redundancy preserves equivalence, strengthens or weakens the specification, or affects joint satisfiability. Problem P12 investigates the criticality of missing information by removing selected clauses from a formula. Removal may be random or biased toward safety or liveness constraints. This enables experiments on robustness, incomplete specifications, and the stability of inferred properties. **Graph Structure and Modularity** Problem P13 controls the topology of the atom co-occurrence graph. Supported structures include: * sparse graphs; * dense graphs; * tree-like structures; * modular structures; * hub-centered structures. This makes it possible to investigate how structural organization of a logical specification affects theorem-proving performance. Problem P14 studies modularity and integration of behavioral models. Multiple modules can be generated with independent, weakly coupled, moderately coupled, or strongly coupled atom sets. The resulting global model supports evaluation of locality, global reasoning, and co-satisfiability. **Conflict and Inference Depth** Problem P15 introduces controlled local inconsistency. Conflicts may be direct, conditional, or behavioral, and their detection may require short or long inference chains. Problem P16 investigates implication depth by generating formulas containing chains of increasing length. Benchmarks can test both transitive derivation and contradiction arising from the combination of the first and last elements of the chain. These problem families support research on explanation depth, conflict localization, and the computational cost of indirect reasoning. **Horn Structure and Phase Transition** Problem P17 studies formulas containing different proportions of Horn clauses. Since Horn structure often enables more efficient reasoning, this benchmark family supports controlled investigation of the transition from Horn to non-Horn specifications. Problem P18 explores reasoning difficulty near the SAT/UNSAT phase-transition region by controlling the ratio between clauses and atoms. This enables experiments on potentially hard logical instances and comparison of solver behavior under increasing formula density. **Supported Provers and Solvers** LOFT provides a common execution environment for multiple automated reasoning engines: * **Vampire**; * **SPASS**; * **E Prover**; * **iProver**; * **Prover9**; * **Z3**; * **CVC4**; * **CVC5**; * **Drodi**; * **InKreSAT**. These tools differ in accepted input formats, reasoning paradigms, and implementation strategies. LOFT hides much of this heterogeneity behind a common benchmark interface. Problems are generated primarily in the TPTP format. Where necessary, the platform automatically invokes dedicated converters: * TPTP FOF to CNF for iProver; * TPTP to LADR for Prover9; * TPTP to SMT-LIB2 for Z3 and CVC5; * TPTP to the native modal format used by InKreSAT. Converted files are cached to avoid repeated processing of identical benchmark instances. **Experimental Workspaces** Experiments are organized into separate **workspaces**. Each workspace stores: * generator settings; * random-seed configuration; * prover timeout; * generated benchmark problems; * converted problem representations; * benchmark results; * execution statistics. A fixed seed can be used to reproduce exactly the same benchmark families, while a random seed supports exploratory generation of new instances. Workspaces allow researchers to maintain independent experimental configurations, compare different benchmark campaigns, and preserve complete execution histories. **Benchmark Execution and Results** The Benchmark module allows the user to select arbitrary combinations of problems and reasoning engines. Each pair consisting of one problem and one prover is treated as an individual benchmark cell. Benchmarks are executed asynchronously and may be processed in parallel. Results are streamed to the user interface in real time and saved in persistent JSON reports. For each benchmark cell, LOFT records: * reasoning result; * real execution time; * system CPU time; * peak memory consumption; * conversion status; * timeout or execution error. Supported result categories include: * SATISFIABLE; * UNSATISFIABLE; * UNKNOWN; * TIMEOUT; * UNCONVERTED. The result interface presents both detailed tables and interactive charts. Researchers can select a benchmark parameter for the horizontal axis and compare execution time or memory consumption across multiple provers. This is particularly useful for scalability analysis and identification of solver-specific performance patterns. **Reproducible Execution Environment** LOFT uses Docker and Nix to provide isolated and reproducible execution environments for individual reasoning engines. Each prover is packaged in a dedicated container derived from a shared base image. Provers are launched on demand rather than running continuously. This reduces resource consumption and avoids the need for a complex microservice architecture. The backend starts the required container, passes the problem through standard input, collects standard output and error streams, and records resource statistics using GNU Time. The use of fixed Nix package revisions strengthens reproducibility by preserving exact software dependencies and prover versions. It also facilitates rebuilding the experimental environment after long periods of time. **Web Application and Command-Line Interface** LOFT provides both a web-based interface and a command-line interface. The web application contains four main workspace views: * **Settings** – configuration of the seed, prover timeout, and syntax checks; * **Generator** – generation and management of benchmark problems; * **Benchmark** – selection of problems and reasoning engines; * **Results** – inspection, comparison, visualization, renaming, and deletion of benchmark reports. The command-line interface supports rapid testing, automated scripts, and integration with external experimental workflows. Core operations include problem generation, syntax checking, and benchmark execution. **System Architecture** The platform consists of the following main components: * **Python backend** – implements benchmark generation, workspace management, prover orchestration, result processing, and the Web API; * **React frontend** – provides the interactive experiment-management interface; * **Problem generators** – implement the P01–P18 benchmark families; * **Prover containers** – provide reproducible environments for individual reasoning engines; * **Conversion tools** – translate TPTP problems into prover-specific formats; * **Benchmark orchestrator** – coordinates parallel execution and real-time result streaming; * **Visualization layer** – presents comparative performance charts and detailed reports; * **Workspace storage** – preserves experimental configurations, generated problems, and results. **Research Scope** LOFT provides experimental infrastructure for research in automated theorem proving, SAT/SMT solving, formal verification, behavioral specification analysis, benchmark engineering, and empirical evaluation of reasoning technologies. The platform can support studies concerning: * scalability of theorem provers; * effects of logical structure on reasoning complexity; * robustness of verification methods; * comparison of symbolic reasoning paradigms; * behavioral specification evolution; * inconsistency and redundancy analysis; * modular and distributed specifications; * explainability and conflict localization; * reproducibility of automated-reasoning experiments. By combining controlled benchmark generation, heterogeneous solver execution, reproducible infrastructure, and comparative analytics, LOFT provides a unified environment for systematic empirical research on logical reasoning methods. Further technical details are available in the accompanying documentation: [[https://drive.google.com/file/d/17A9aOnENue4-2rWLOmRKc76gvN97eza1/view?usp=drive_link]]. **RE-IDE** Workflow-driven requirements engineering environment supporting structured model generation, clarification, validation, and preparation of artifacts for formal verification. ===== Programme Summary ===== The programme integrates software engineering, requirements engineering, formal methods, process mining, automated reasoning, and AI-assisted development. Its central objective is to move from artifact-level correctness toward explainable and verifiable reasoning about system behavior.