The notion of covariant-contravariant refinement (CC-refinement, for short)
is a generalization of the notions of bisimulation, simulation and refinement.
This paper introduces CC-refinement modal $\mu$-calculus (CCRML$^{\mu}$)
obtained from the modal $\mu$-calculus system K$^{\mu}$ by adding CC-refinement
quantifiers, establishes an axiom system for CCRML$^{\mu}$ and explores the
important properties: soundness, completeness and decidability of this axiom
system. The language of CCRML$^{\mu}$ may be considered as a specification
language for describing the properties of a system referring to reactive and
generative actions. It may be used to formalize some interesting problems in
the field of formal methods.

本文介绍了一种新的模态 mu - 演算系统 CCRML^μ，该系统由模态 Mu - 演算系统 K^μ 添加 CC-refinement 量词而得到。CCRML^μ 可用于规范化一些关于反应和生成动作的系统性质的问题，是一种描述系统性质的规范语言。此外，本文还通过一些重要性质（如正确性、完备性、可判定性等）的探究，给出了 CCRML^μ 的公理系统。

协变 - 逆变细化模态 $μ$- 演算

Covariant-Contravariant Refinement Modal $μ$-calculus

Predictive analysis in business process monitoring aims at forecasting the
future information of a running business process. The prediction is typically
made based on the model extracted from historical process execution logs (event
logs). In practice, different business domains might require different kinds of
predictions. Hence, it is important to have a means for properly specifying the
desired prediction tasks, and a mechanism to deal with these various prediction
tasks. Although there have been many studies in this area, they mostly focus on
a specific prediction task. This work introduces a language for specifying the
desired prediction tasks, and this language allows us to express various kinds
of prediction tasks. This work also presents a mechanism for automatically
creating the corresponding prediction model based on the given specification.
Differently from previous studies, instead of focusing on a particular
prediction task, we present an approach to deal with various prediction tasks
based on the given specification of the desired prediction tasks. We also
provide an implementation of the approach which is used to conduct experiments
using real-life event logs.

该论文引入了一种用于指定预测任务并自动创建相应预测模型的规范语言，以应对不同业务领域的预测需求，并提供了实现该方法的实验结果。