在并发系统的研究领域，时序逻辑常被用来刻画和推理并发系统的性质及行为。时序逻辑包括线性时间时序逻辑、分支时间时序逻辑及偏序时序逻辑三类，其中，偏序逻辑具有较强的刻画能力，主要体现在三个方面：偏序逻辑可以更加忠实的刻画并发特性；偏序逻辑允许直接刻画涉及原因、矛盾和并发的性质；更为重要的是，它缓和了系统验证时的状态爆炸问题。 事件结构逻辑是最基本的偏序时序逻辑之一。人们为了刻画系统的并发现象，发展了多种事件结构逻辑，并建立了其证明系统。然而在刻画反应式系统时，现有的事件结构逻辑却存在以下三个不足：表达能力不足，无法刻画涉及多诱因特征的反应式系统行为；用来对反应式系统建模的事件结构模型较为庞大：无法刻画反应式系统的动作行为。为了解决这种现象，我们对事件结构及其逻辑体系进行了深入研究。 针对传统事件结构逻辑的第一个不足，我们提出了一种流事件结构逻辑FESL(Flow Event Structure Logic)。传统的事件结构逻辑体系之所以不能刻画多诱因特征，就在于它的语义框架建立于基本事件结构之上，我们在FESL中，摒弃了传统的基本事件结构，而采用能刻画多诱因现象的流事件结构，因而能够刻画多诱因特征。为实现对反应式系统行为的推理，我们为FESL建立了合理而且完备的证明系统。 针对第二个问题，我们深入研究了事件结构的对称性，力图从结构上建立对建模语言和模型进行约简的基本理论。对于事件结构模型，我们提出了基于置换群的对称性概念。在事件结构中，引入了事件结构的商结构模型，证明了商结构与原事件结构是迹、互模拟和偏序多集迹等价的，建立了针对事件结构的对称约简算法，得出了对称约简不影响等价在动作细化下的保持。在研究了事件结构的对称性之后，进一步从理论上比较对称约简与自互模拟约简的区别和联系，并将对称约简应用于事件结构逻辑的模型检测之中。 针对传统事件结构逻辑无法刻画反应式系统动作行为的不足，我们建立了两种基于动作的事件结构逻辑EESL[C]和aESL。这两种逻辑分别采用了不同的动作观点，以适应不同的刻画需求，建立对应的逻辑体系。EESL[C]是带有并发算子的事件结构逻辑ESL[C]的一个动作扩展。在EESL[C]中，我们定义了一个原子动作公式的集合，分别对应于每一个原子动作，从而在逻辑层次上将动作行为与状态建立了联系。 aESL则采用了动作序列的观点，在这一逻辑体系中，我们并不考虑单一的原子动作公式。我们将所有的动作行为看成是一个动作序列，对动作序列带来的状态变化进行了分析。同时，影响逻辑为真的条件不再仅由状态公式是否得到满足来表示，动作行为是否满足同样会影响到公式的可满足性。如果系统刻画中的某个动作序列不能在当前事件中得到满足，则该刻画公式为假。 同时，我们分析了EESL[c]和aESL之间的区别和联系，证明了EESL[c]是aESL的一个子集，并且aESL中的顺序动作联结符和冲突动作联结符可以转化为EESL[C]中的动作行为。 本文的最后，我们将事件结构的对称约简应用到反应式系统的模型检测中，定义了反应式系统基本迹的概念，讨论了基于基本迹，构造反应式系统的事件结构、及其商结构的方法。