Radosław Klimek

Ta strona jest tylko do odczytu. Możesz wyświetlić źródła tej strony ale nie możesz ich zmienić.
====== 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.

<code>
Requirements
    ↓
Behavioral Models
    ↓
Logical Specifications
    ↓
Verification
    ↓
Diagnostic Explainability
    ↓
Behavioral Accountability
</code>

===== 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". Available https://drive.google.com/file/d/16Jv_s1as1nyTmG_fGRpZIMyQD0ZCEXJd/view?usp=sharing
Workshop conference paper, Rank A, 140 pkt MNiSW, under review.

**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, 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". Available at: https://drive.google.com/file/d/1BPOiJOxaOxiZXbeJBofehkj7kp5c-2fk/view?usp=sharing.
Conference paper, Rank A, 140 pkt MNiSW, under review.

**Diagnostic Explainability**

[Kli Bla 26] Radosław Klimek, Jakub Blazowski “Towards Diagnostic Explainability inWorkflow Verification via
Shapley Attribution”. Pre-print version available at https://arxiv.org/abs/2512.09562
Flagship conference Core Rank A*, 200 pkt  pkt MNiSW, under review.

[Kli 26] Radoslaw Klimek "Toward Defensible System Behavior in AI-Assisted
Software Engineering". Available at: https://drive.google.com/file/d/1Kd27tbguuhNDsPEkscktOx6oEAAwgMJi/view?usp=sharing.
Conference paper, Rank A, 140 pkt  pkt MNiSW, under review.

[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/1rjYP3S3yKVl0RNMSl3Ft5rxyP2uoyd2N/view?usp=sharing and also https://drive.google.com/file/d/1qkMWiD381YzMZrXgdPyGwyBBfZcaf-Z-/view?usp=sharing
Conference paper, Rank A, 140 pkt  pkt MNiSW, under review.

[Kli 26c] Radoslaw Klimek "A Workflow-Based LLM Assistant for Iterative and Verified Requirements Engineering". Available at: https://drive.google.com/file/d/1QgdzVxNvLCtg3BBg6fElI0x_rLc-jIRt/view?usp=sharing.
Workshop conference paper, Rank A, 140 pkt  pkt MNiSW, under review.


**Others / Adjacent Research**

[Kli 26e] Radoslaw Klimek "Context-Aware Orchestration of Adaptive Decisions in Intelligent Environments". Available at: https://drive.google.com/file/d/1Jv_oO5OFf8t2cbTlOfYDvOcDNYHHHnUT/view?usp=sharing.
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/1n5uMnilJrz0yGkkBc4aRcXy8pgZ8Aee1/view?usp=sharing.
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. 

**LIGIMINE**

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.

**LOFT**

Another key component is LOFT (Logical Framework and Testbench), a benchmark generation and experimentation environment for automated reasoning in software engineering. LOFT supports the generation and management of logical verification problems, including satisfiability, consistency, implication, redundancy, conflict detection, behavioral constraints, and theorem-proving tasks. The framework enables the construction of benchmark families with controllable structural properties, facilitating systematic evaluation of theorem provers, SAT/SMT solvers, and logic-based verification methods.

**ATP Benchmark Collection**

The infrastructure further includes the ATP Benchmark Collection, a benchmark suite of automated theorem proving problems derived from software-engineering-oriented behavioral verification tasks, and the Logical Problem Catalog, a curated repository of logical verification problems involving behavioral models, workflow specifications, consistency checking, satisfiability analysis, property validation, implication reasoning, and behavioral diagnostics. Together, these platforms and resources provide an experimental foundation for advancing explainable and verifiable behavioral engineering through reproducible evaluation, benchmark-driven research, and prototype validation.


**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.